RE: Using jEdit properties (WAS: Re: [ jEdit-devel ] [Patch]ClassWizard plugin compiles yet with jEdit4.0pre1(CVS))

[John G. <jge...@ny...>]

> Thanx Dominic,
>
> > The properties file $HOME/.jEdit/properties overrides that of jEdit and
> any
> > properties files for plugins so a user could add this to that properties
> > file. In fact any properties you set with jEdit.setProperty(...) are
> stored
> > in this file not the files in the jars.
> > The only problem with users adding things top this is that it is not
> > sorted/doesn't have comments so it is hard just to look through.
> >
> > Best Wishes,
> >
> > Dominic Stolerman
>
> So, following my point, if I want to give users some sort of  ability to
> edit their settings, best way is to use ClassWizard's own property file -
> just as it is now, corect ?
>
> TIA,
> philip
>

There are two other approaches that don't require an extra properties file
to manage:  one is to place calls to jEdit.setProperty() in a startup
script.  The startup scripts are called after properties are loaded from all
the jar files.  The second is to use a macro I just posted on jEdit
Community, Edit_jEdit_Property.bsh, which gives you a simple GUI for
examining and editing a given property.  Unlike editing a properties file,
this will let you change a property on the fly. Of course, you can do all
this with individual BeanShell commands, but the macro's dialog provides
immediate verification of a change.

The installation macro Misc/Properties/jEdit_Properties dumps all of the
application properties into a new buffer.  You can then search the buffer
(before or after invoking Sort Lines from the default right-click menu) to
find what you need quickly.

You can decide what is best for your plugin, but here are all the options.

JOhn