[ jEdit-devel ] [ jedit-Bugs-3414877 ] Extra vertical line spacing bug

Bugs item #3414877, was opened at 2011-09-28 09:54
Message generated for change (Tracker Item Submitted) made by tvojeho
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=100588&aid=3414877&group_id=588

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: editor core
Group: minor bug
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: tvojeho (tvojeho)
Assigned to: Matthieu Casanova (kpouer)
Summary: Extra vertical line spacing bug

Initial Comment:
Hi, 

when using the feature "Extra vertical line spacing" on Text Area option pane, there are two cosmetic issues I noticed:

1) When scrolling with Down Arrow with extra spacing in negative values, each time the cursor jumps on a new numbered line, it leaves a small mark where the upper part of the cursor was - I guess it would be the size of pixels set in the options.

2) Selecting text - the text selected is in the original place it would originally be while the the unselected text remains in the place determined by the line spacing options, thus the text line creates a "step up/down".

tvojeho

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=100588&aid=3414877&group_id=588