On Mon, 18 Nov 2013 07:40:24 -0800 (PST) jquil...@gmail.com wrote: > On Monday, November 18, 2013 4:12:52 PM UTC+1, Terry wrote: > > > I don't know what Edward did with myLeoSettings.leo a couple of weeks > > back, but you, Jerry, I think were just reporting that the menu > > (non)highlighting bug returned when you compiled the stylesheet from > > the outline with the script? I'll look in to that. > > Yes, that's what happened. I had to delete the whole theme, and copy it > anew from leosettings.leo.
I can't reproduce that, starting with an empty $HOME/.leo and creating mySettingsLeo.leo and copying in dark theme 0 and Ctrl-B on the "source & stylesheet" node does not remove menu highlighting for me. Haven't been able to test in Win 8. > However, the problem of unnecessary complexity still remains: just count > how many times the same parameter may be defined in the settings. It's > quite confusing, especially for those who not used to it. This, as I > explained in an earlier post, may results in a lot of frustration, when you > change the setting in one location, expecting to see the change appear the > next time the program restarts, and that's not what happens! > The straighforward way of managing the settings, in my NEWBIE opinion, > would be to have each setting appear one time only. I think I need to spend more time weeding and less time on this email thread :-) > By the way, is it possible to implement the settings without having to > restart Leo? I think for style type things that should be possible, it sets the new style on the fly now, but it can get re-set to the version it found at load time later on in that session. It should be possible to push the new value back into the runtime settings db. This isn't the case for a lot of other settings stuff, as Edward says it gets copied into various runtime places. Cheers -Terry -- 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 post to this group, send email to leo-editor@googlegroups.com. Visit this group at http://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/groups/opt_out.
