On Mon, Aug 1, 2011 at 10:43 AM, Terry Brown <[email protected]> wrote:
> I should have made it clearer that those are the first choice in my
> response too. It depends on the nature of the data being stored and
> how it's going to be written to the storage place. I don't think there
> are mechanisms for writing to the @settings trees other than hand
> editing by the user?
That's correct. Only hand editing exists.
> Maybe a useful command would find the active location of a specified
> @setting and bring up that .leo file with the cursor at that position.
Awhile back Kent asked for g.app.config_iter. For example, here is
the heart of the print-settings command:
for name,val,c,letter in self.config_iter(c):
kind = g.choose(letter==' ',' ','[%s]' % (letter))
result.append('%s %s = %s\n' % (kind,name,val))
The letter field tells where the setting comes from. This is fine,
except that it doesn't tell exactly where, so maybe the script/command
would need to look at the table in readSettingsFiles and its helpers.
It's baroque, to say the least...
> So a plugin could include in its Plugins menu submenu an "Edit Prefs."
> command which the plugin would write as a simple
> c.edit_config('myplugin_option_a').
> Leo would then open the @settings file containing the active instance
> of the myplugin_option_a option selected. The plugin could put all its
> settings in an organizer node so that 'myplugin_option_a' was the first
> of them, ensuring that all the plugin's options are presented.
>
> Get's confusing if the user had split the plugins options between
> leoSettings and myLeoSettings, maybe
> c.edit_config(['myplugin_option_a', 'myplugin_option_b', ...]) could help.
>
> Core Leo could also use this mechanism for context dependent pref.
> editing.
I personally do not think the massive effort required is anywhere near
being useful enough.
Edward
--
You received this message because you are subscribed to the Google Groups
"leo-editor" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/leo-editor?hl=en.
