How can I find out, where on SF this is maintained? I did a search on SF for the word "Optional.jar", but nothing came out. When I do a search on "Optional" (without .jar), I get TONS of results.

The jEdit Bug Trackers are found at http://sourceforge.net/tracker/?group_id=588 . You'd have to create a SourceForge account.

Robert

For me, the Optional Plugin works perfect. Please ensure, that You have installed the current version of the plugin (it's 1.0).

If so, maybe You should delete the jars-cache subdirectory of Your jedit's settings directory or the whole settings directory...

Robert

I have 1.0 too.

I would hate to delete my whole settings directory, because I would have to recreate then all the settings, but I have delete the Optional.jar.summary file from the settings directory; but still the error persists.

Ronald

Though it's not nice that jEdit hangs, I really think that Your problem isn't a bug in the Plugin. So, please try to exclude the influence of the settings directory first.

Of course You don't have to delete the settings directory physically - just rename it, when jEdit isn't running.
In case of success You only need to copy Your old "properties" file to the automatically re-created directory. Maybe there are some more files You want to copy from the old directory. But most of the files are not needed.

Robert

Indeed, cleaning the settings dir brings more insight of what happened:

With a fresh settings dir, installing just Optional.jar and bringing up the plugin options, has the effect that instead of the normal option window is displayed, which has a height of only the title bar (so that it looks as if the window were minimized to the title bar only. I can, however, enlarge that window using the mouse and see all the options. So the "bug" here is only that the plugin option window is not fully shown.

My guess now what had happened to my original installation:

In my settings, I have used a different skin, a slightly different font, etc., and when I called the plugin options, the tiny plugin window was probably created, but - maybe due to the different geometry of the main window - being placed *behind* the main window. So I had the main window in front and the Plugin Options window (which had the focus) in the back. No way to bring it to the front.

So why did the Plugin Options dialogue and up in the back of the main window? If it was not designed that way, it could be because on my system, I have "focus follows mouse" enabled. Likely the tiny plugin options window *was* created in front of the main window, but my mouse cursor was at that time still on the upper part of the main window, where I had clicked on the "Plugin/Plugin Options" menu entry; so, because of "focus follows mouse", the main window was brought in front, but the plugin options window still kept the focus. Kind of a deadlock situation.

A solution to this problem would be to create the plugin options window non-modal, but I guess this has deeper impact into the design of jEdit.

Still it puzzles me why the presence of Optional.jar causes the Plugin Options window being created so small. If it were larger, chances are good that it would not be covered totally by the main window, and it would be easy to bring into front.

Ronald

I've seen the minimized Optional window, too. I think this is the case, when there are no settings for the Optional plugin yet. It's not nice, but it hasn't been a problem for me.

I'm sure that the options dialog must be modal to avoid interferences between editing and changing settings.

You could file a bug report about the window size. But if You could reproduce the deadlock situation it may be better to report this with exact system information.

Robert

Another possibility would be to take care about the placement of that window. I understand that is causes trouble making it non-modal, but then it could be placed so that it is not covered entirely by the main window - for example, by placing it always to the top left of the screen unless the main window occupies this place already, in which case it can be placed to the bottom right position of the screen. Of course we still would have a problem in the cases when jEdit occupies the whole screen, but I think there is easy solution to this special case.

Ronald