#63 Updates to BufferSelector to use the new API/fixes
Attached is a version of BufferSelector which uses the 'new' version of the plugin API. This plugin fixes/updates a few things.
* Added a horizontal and vertical gap option within the options pane.
* Created a basic skin that is less 'chromy' and more consistent on OS X.
* Simply by recompiling I seem to have fixed the issue where BufferSelector would not update to reflect the contents of the buffer.
This update changes the way the menus work. Before there was a checkmark next to the name of the plugin that displayed based upon whether the BufferSelector was enabled on the view. I could not find a way to update this checkbox at startup. Additionally there is a race condition where the EditAction's isSelected() beanshell would execute before the action's beanshell would finish. So I removed the checkbox.
Lastly, there have been no updates to BufferSelector since 2002. There is no branch in SVN, I grabbed the source from a SF tarball. If there is no maintainer for this plugin, I would be glad to take on the responsibility.
This is not a patch, and bufferselector is now updated to jedit 5.x.
If you want to submit additional enhancements, please check it out from the Git repository, where it is now.