#3717 Extra vertical spacing should not be applied to first line
The gutter text lines do not align with the text lines of the text area when extra vertical spacing is configured. See the screenschot in attachment, there is a (in my case) downshift of the gutter. Since it is a constant downshift, that does not accumulate N pixels for every line, it is not much of a bother, still it's a bug :)
Using jEdit trunk snapshot 2012-06-11_12-02-24. In the screenshot, i'm using Look&Feel, but I've retried without the plugin and the downshift is still there. (by the way, if that matters, I'm using Consolas 10 pts in the text area and Consolas 9 pts in the gutter, Windows XP)
I guess that, since every gutter line has to be synced with the matching text area line (and since font vertical size is different), a "vertical sync" is applied independently to each line. Which means that this "sync" does not apply extra vertical spacing - which should explain why the downshift does not accumulate.
vertical line spacing and gutter
I'm such a loosy tester :)
I should have seen from the start : the bug is that the vertical spacing is applied to the first displayed line in the text area, but it should be applied only beginning from the second line. It is the text area that is "upshifted" in my exemple, not the gutter that is "downshifted" (it is not very clear on the screenshot, I have cut it a bit too much).
Changing the tracker "summary" to be correct.
Thus, I guess that the problem I have with selection background and Plugin Highlight are caused by this first line vertical spacing. Maybe not, but fixing the text area first line might improve the rest...
Fixed in revision 23977.
Thanks for taking the time to fix the bug. I used the updater plugin to get the daily build ; things are much more usable ; alas, this does not work completely with blinking cursors and selection.
When blinking cursor is activated, the first time the cursor steps into a line (e.g. I click on a line, or move the cursor with keyboeard arrows), things are fine. But as soon as the cursor disappears, the line number in the gutter for the line steps down. When the cursor blinks back, the gutter stays down. If I then move the cursor into another line with a mouse click, the line number in the gutter returns to its initial (correct) position. If I move the cursor to the next or previous line with keyboard up/down arrows, the gutter number of the line I left stays down. I guess keyboard and mouse movements trigger different text area repainting...
Independently from cursor blinking, if I click with the mouse button to select text, whether a part of a single line or a multi-line selection, the line number(s) for the selected line(s) also move. And they move back when I release the mouse button.
Playing with cursor settings, I just saw that a "block cursor" is also a bit down (and thus the cursor hilighted at the end of a fold is also down)... But it's not related to the gutter bug.
I can only guess combining the vertical spacing feature with all other text area features is hard to implement correctly. I love the vertical spacing feature (it gives me more lines on my screen), but I can live with some quirks if you have other bugfixing/feature priorities (that I can understand).
Revision 23977 indeed causes odd problems, when the gutter is partially repainted (e.g. moving the cursor up or down). Here is an alternative approach: http://isabelle.in.tum.de/repos/isabelle/file/3df1b6a5837c/src/Tools/jEdit/patches/gutter
Fixed in revision 24165, I tested with both positive and negative line spacing, and the gutter lines seem to be aligning properly with the text area lines without any shifting up or down.