On Mon, Dec 19, 2016 at 3:02 PM, Mike Hodson <myst...@gmail.com> wrote:
> On Mon, Dec 19, 2016 at 12:40 PM, Largo84 <larg...@gmail.com> wrote: > >> Jon, I use these options all the time. In fact, they're in my desktop >> shortcut link (Windows). Maybe this helps: >> >> Target: C:\Python34\python.exe "D:\Synced\github repos\leo\launchLeo.py" >> --session-save --session-restore >> > > I'd personally appreciate some setting that can be effected with Leo's GUI > only. It is entirely non-intuitive to have a gui without all options > exposed inside of it. > The situation is different as far as Leo is concerned. In fact, all settings *are* "exposed" in the gui, but not in the usual way. To see all options, choose Settings:Open Global Settings. This opens leoSettings.leo. This strategy is far superior to typical ways of specifying settings, either .ini files or graphical displays of settings. Maybe more than 10 years ago I experimented with panels by which users could set settings. It was a failure, and I ripped out the code. The problem is that Leo's settings are much more flexible than in other environments. Plugins and scripts can, and do, define their own settings. Furthermore, the ability to organize (and search) myLeoSettings.leo would not be possible with gui-oriented approached. In short, the present settings scheme, although not without minor problems, is a good fit for Leo. It's not going to change. Edward P.S. The sessions command-line arguments could be specified in myLeoSettings.leo, but that might turn out to be more confusing than the present scheme. Having said that, I would be willing to consider specific enhancement requests re sessions. EKR -- 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 https://groups.google.com/group/leo-editor. For more options, visit https://groups.google.com/d/optout.
