|
From: Damien R. <dam...@gm...> - 2010-01-30 23:34:36
|
I wrote a small macro that attempts to clear all unused properties from jEdit. It works by maintaining a list of properties to keep using a set, then iterating through all of the defined properties and unsetting any not contained in the set. Properties to keep are determined by reading through some property files defined in the jedit jar (jedit.props and jedit_gui.props), properties with a special ending (currently just .shortcut and .dock-position), anything saved in a plugin's cache, and a few are added manually. From my quick tests it appears to work fine with no adverse effects, but I wanted to see how it works for others, and if it's stable enough then maybe include it with jEdit. Hopefully this will help speed up jEdit for anyone who's getting bogged down with a lot of unused properties. |