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.
|Submitted||alf456 - 2012-06-26 - 07:19:21z||Assigned||nobody|
|Priority||5||Category||text area and syntax packages|
|2012-07-26 - 09:41:47z
|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...
|2012-06-26 - 07:19:25z
vertical line spacing and gutter