From: Andrew B. <and...@ma...> - 2011-08-21 12:04:35
|
I want to have a number of settings directories. However I would liketo have a number of plugins in the system settings directory. Is it just a case of moving the jars to this directory, or can I use plugin manager to install directly there. What happens about settings - should I be copying the settings from the <user>/properties file to a properties file in the <system>/properties/ directory. |
From: Robert S. <Rob...@ka...> - 2011-08-21 12:57:32
|
Hi, here are a few general hints to get a jEdit installation, which is partial user-independent. First, I guess You mean: - "jEdit program directory" alias "JEDIT_HOME" when saying "<system> directory" - "jEdit settings directory"alias "~" when saying "<user> directory", don't You? There are 3 things to deal with: 1. Plugins a) Installing a plugin is just copying the jar. You can do it manually, but the Plugin Manager handles dependency plugins for You. b) It doesn't matter, whether a jar is installed in program or settings directory, except the latter are only loaded for the current user. c) In "Global Options -> Plugin Manager" You can set where Plugin Manager should install plugins 2. Properties Most settings of jEdit core and plugins are stored in the ~/properties file. You can extract any property out of this file into any numbers of files with ".props" extension and move them into JEDIT_HOME/properties directory. So, these properties are present for all users, but can be overridden from personal settings in ~/properties file. 3. Plugin settings Some plugins store certain settings in subdirectories of the settings directory both in property and xml files (i.e. Projects of ProjectViewer). I guess You can't make them available for all users. At least I haven't tried this. Robert |
From: Andrew B. <and...@ma...> - 2011-08-23 17:28:00
|
Thanks for the reply. Sort o thing I was looking for ... On Sun, Aug 21, 2011 at 02:59:06PM +0200, Robert Schwenn wrote: > Hi, here are a few general hints to get a jEdit installation, which is partial > user-independent. > > First, I guess You mean: > - "jEdit program directory" alias "JEDIT_HOME" when saying "<system> directory" > - "jEdit settings directory"alias "~" when saying "<user> directory", don't You? In practice yes. I am actually planning on running on windows and running more than one config under the same user using a command line switch : -settings="%USERPROFILE%\.jedit_exp" > There are 3 things to deal with: > > 1. Plugins > a) Installing a plugin is just copying the jar. You can do it manually, but the > Plugin Manager handles dependency plugins for You. > b) It doesn't matter, whether a jar is installed in program or settings > directory, except the latter are only loaded for the current user. > c) In "Global Options -> Plugin Manager" You can set where Plugin Manager should > install plugins Ah - I hadn't spotted that. Is it OK to install some plugins globally and then change it to do more plugins locally. I notice the following properties and wonder if this might cause confusion : plugin-blacklist.FTP.jar=false |
From: Robert S. <Rob...@ka...> - 2011-08-23 19:14:19
|
> Ah - I hadn't spotted that. Is it OK to install some plugins globally > and then change it to do more plugins locally. > Yes. > I notice the following properties and wonder if this might cause > confusion : > plugin-blacklist.FTP.jar=false > You don't have to care about them. When You delete them, they will be there next time :-) Robert |
From: Vampire <Vampire@jEdit.org> - 2011-08-24 01:20:01
|
Andrew Black schrieb: > Ah - I hadn't spotted that. Is it OK to install some plugins globally > and then change it to do more plugins locally. > You should just make sure you don't have global plugins that depend on local plugins that are not available for all settings directories, otherwise you will get an error message when starting with the settings directory that doesn't have the dependencies installed. > I notice the following properties and wonder if this might cause > confusion : > plugin-blacklist.FTP.jar=false > This is just the checked state in the plugin manager. If you uncheck and thus unload a plugin it will stay unloaded even if you restart. For those plugins the respective property is set to true. It doesn't matter where that plugin is installed. So you can even disable global plugins by local config. Regards Vampire |