[ jEdit-devel ] Clear Properties Macro

[Damien R. <dam...@gm...>]

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.