My problem with this is not individual settings like font size, but that I don't know how to modify them. I tried copying specific settings to myLeoSettings.leo under a new node @theme Default, but they don't take effect. When I open myLeoSettings.leo, then I seem to get some kind of strange hybrid between my old settings and the new theme. This isn't really workable for me.
Also, when I use the menu item Settings/Edit A Theme File, the theme file opens in a new modal Leo window and the original Leo window is inactive. So I wouldn't be able to copy and paste any settings but only to modify the existing theme. I don't want to modify the default theme file or my changes would be lost every time I use a new version of Leo. On Sunday, October 11, 2020 at 7:15:48 AM UTC-4, Edward K. Ream wrote: > > This is part of #1663 > <https://github.com/leo-editor/leo-editor/issues/1663>. I may "refactor" > that issue into separate pieces. > > The new code is in devel. You can test it by temporarily removing your > myLeoSettings.leo. > > The new code enables DefaultTheme.leo by default, and makes DefaultTheme a > dark theme: > > - leoSettings.leo now contains @string theme-name = DefaultTheme > - DefaultTheme.leo is the same as EKRDark.leo, except for a smaller font > size. > > Imo, the new default look is significantly better than the old "light" > look. > > *Remaining questions* > > What should the default fonts be? At present, the default font is DejaVu > Sans Mono, which may be problematic on some platforms. > > DefaultTheme.leo contains a top-level clone for the "Fonts & text sizes" > organizer node, so it is easy to see these settings, but newbies probably > won't know that. > > Your comments please, Amigos. > > Edward > -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/fdb05b87-f11f-41b7-80a0-447b8d468ddfo%40googlegroups.com.
