PreviousNextTracker indexSee it online !

(170/212) 456 - site-wide folder for modes, macros and plugins that is not clobbered by upgrades

Background: we have 2 separate installs of jedit tailored for 2 different workfows (multi-user). Attempting to merge them using '-settings=/some/where/else' command-line switch:
dmaziuk@stingray:~$ java -Xmx96m -Xms24m -jar /share/java/jEdit/5.0.0/jedit.jar -noserver -settings=/share/java/jEdit/mrannotator/
12:56:25 PM \[main\] \[error\] main: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/activity.log (Permission denied)

After making that a+w:
PluginJAR: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/jars-cache/QuickNotepad.jar.summary (No such file or directory)

and
IOUtilities: Error moving file: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/properties (Is a directory) : /share/java/jEdit/mrannotator/properties (Is a directory)
12:57:18 PM \[AWT-EventQueue-0\] \[error\] jEdit: Failed to rename "/share/java/jEdit/mrannotator/#properties#save#" to the user properties file "/share/java/jEdit/mrannotator/properties"

So clearly '-settings' overrides "user.home/.jedit" -- why have it in the first place when I can just 'java -Duser.home=/some/place/else' ?

Or should I file a feature request for (e.g.) '-global-settings=' switch instead ?

Submitted dmaziuk - 2013-01-07 19:14:45 Assigned
Priority 2 Labels
Status open Group none
Resolution None

Comments

2013-01-07 19:33:55
ezust

You are getting permission denied messages because of permissions problems, and you're trying to use a shared area for settings that are used by multiple users at the same time?
It is possible to put some site properties in the jedit home directory, if you want to share settings between multiple users, but a user settings directory must be owned by that user and only used by one user at a time.

What platform is this?


http://www.jedit.org/users-guide/settings-directory.html

Site Properties

You may also put properties files in the "properties" directory in the jEdit home directory (NOT the .jedit settings directory). You can locate the jEdit home directory by going to the Utilities menu directory, then the "jEdit Home Directory" menu item, and the first item in the pullout menu will be the location of the jEdit home directory. This is intended for site-wide settings and it is useful for things like a set of custom key bindings that you might want to share between different computers. This lets you keep your custom properties separate from the jEdit properties, so they are easier to find, edit, and move between machines. Note that your custom properties files must have ".props" as the file name extension.

Site properties files are read in alphabetically by file name. This means that if you have a property with the same name in more than one file, the value for that property will be the value found in the last file that was read.

You can edit these files inside jEdit - changes made to these files will not be re-read until the next time jEdit is started.

2013-01-07 19:58:10
dmaziuk

What I'd like is to share a set of modes, macros, and plugins between different \*users\*. Specifically, a user working on file type X today will have the macros and modes for X. Tomorrow they'll work on file type Y and have the plugins and modes for that.

I guess on second thought it'd take both '-global-plugins/-global-modes/-global-macros' for what I want and properties for plugin toolbar & docking settings... assuming the user's properties add to the "site" ones -- the README doesn't look like they do.

The platform is linux and yes, I am familiar with unix permissions and I know what the error messages mean.

2013-01-07 21:09:52
ezust

There is a shared set of modes, macros and plugins in jEdit's home directory. You can customize different jEdit installations that way. What is the harm of having jedit.jar and documentation there too?

Also, that error message I see in the original ticket seems to indicate that a directory called "properties" is being opened as a file and failing. perhaps you should rmdir that folder and let jEdit create a properties file.

2013-01-07 22:22:04
dmaziuk

So the two currently available options is to have 2 separate jEdit installs & remeber to upgrade it ttwwiiccee, or have all plugins, macros, and modes available to everyone through the menus -- but use custom '-settings' to turn on and off the relevant UI elements.

I think #2 works as long as there's no filename conflicts in the plugins and modes.

I also realised it's moot because we can't run our custom code on 5.x without updating it (cleaning up BufferChangeListeners and who knows what else) and that's not happening anytime soon. And if you do get a featuire in, it's not getting added to 4.2 (that we run), so it'll be of little use to me.

So anyway, an option tro read plugins/modes/macros from a different global directory may be worth having, or maybe not.

2013-12-09 19:03:15.464000
ezust

- **summary**: sharable common user settings directory --> site-wide folder for modes, macros and plugins that is not clobbered by upgrades
- **Group**: --> v4.3
- **Priority**: 5 --> 2

2013-12-10 18:12:23.849000
dmaziuk

Well, in "mode 1" I use plugin X with 2 windows docked to the bottom and left, and in "mode 2" I use plugin Y with 2 windows docked to the bottom and right. The issue is I don't want X and Y's windows there at the same time. So at teh very least you'd have to package buffer properties like window docking in addition modes and macros to make it a complete solution.

Which still leaves the potential for some obscure conflict between the plugins themselves.

Anyway, as I said before you can already handle the local settings with "-Duser.home=/somewhere/else". The ability to do the same with site-wide settings could be handy and shouldn't be too hard to implement -- you just need to read a command-line switch or -D'ed property and fall back to the hardcoded path if it's empty.

There's a "-settings" switch that either was intended for something entirely dfferent or (and?) it doesn't work in real life.

2013-12-10 18:18:17.979000
ezust

Another option is to use the JVM argument,
-Djedit.home=/path/to/your/global/jEditStuff
perhaps your jedit script can use the same jEdit.jar and different
set of macros/site settings/plugins that way?
If you're using jEdit 4.2, this might be your best bet.

2013-12-10 18:22:49.077000
ezust

Also, your trick of overriding user.home might work fine on Linux but it won't work well on other platforms or in future versions of jEdit.
the -settings directory is really what you are supposed to use. But I can't speak for jEdit 4.2 since we don't support that.