#179 Minimap option to remember divider location

[Dan Higgins]

Hello jEdit Fellows. I really like the Minimap plugin, but it was driving me crazy by resetting the position of the divider, between the buffer and minimap, every time I changed a buffer option.

This patch adds a single new option to set a global value for the location of the divider. It works great for me. Leaving it blank or 0 retains the previous behavior.

[Matthieu Casanova]

Hi, the idea is interesting, but saving the divider location is not a good option if you have the minimap on the right because if you enlarge your window, the minimap will become huge.
I think storing the minimap width would be more useful.
Also it would be nice to save the divider location automatically when it is moved instead of doing it in the option panel.

[Matthieu Casanova]

Ticket moved from /p/jedit/patches/579/

Can't be converted:

• _milestone: