It looks like the themes are supplanting font info but not anything else. For example, if I specify a setting in a theme file it gets overridden by myLeoSettings.leo which is the expected behaviour. Having the font info in a theme override that is inconsistent but could/should be offered as a choice. Or we should pick one way of doing it and eliminate the choice.
I have always thought it rather puzzling to have self-contained themes and then an entirely different way to set fonts. My preference is to set everything related to UI in the theme. I think that choice is Leonine. Whenever I propose a new way to do something I try to phrase it such that there should always be an @bool to offer choice so people can bend Leo to their own preferences. I believe that the default should be the theme as it gives new users one place to go to modify their UI experience. I have totally ignored the entire "other way" as it may well be someone else's preference. But for new users, it is terribly confusing. Chris On Tue, Aug 20, 2019 at 6:50 AM Edward K. Ream <edream...@gmail.com> wrote: > > > On Tue, Aug 20, 2019 at 8:32 AM Matt Wilkie <map...@gmail.com> wrote: > >> A structural problem: theme font-size overrides myLeoSettings.leo, which >> I assume applies for all settings. I expect myLeoSettings to always have >> the last say. >> > > Hmm. I'm not sure what I expect. > > 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 leo-editor+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/leo-editor/CAMF8tS03aB3BDf%3DTDKei80NCXWrw61Tpq2bYN3UBQ_iPrn%3DV9Q%40mail.gmail.com > <https://groups.google.com/d/msgid/leo-editor/CAMF8tS03aB3BDf%3DTDKei80NCXWrw61Tpq2bYN3UBQ_iPrn%3DV9Q%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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 leo-editor+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/CADWQas0RPe-Qsm3%2Ba1rYkb%3D_v496KFKZRXZkMnPd1-A%3DmPp2-g%40mail.gmail.com.
