equal
deleted
inserted
replaced
|
1 diff -ru 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java |
|
2 --- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 2015-10-20 19:56:03.000000000 +0200 |
|
3 +++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java 2015-11-24 21:58:47.686343684 +0100 |
|
4 @@ -185,8 +185,6 @@ |
|
5 } |
|
6 |
|
7 int y = clip.y - clip.y % lineHeight; |
|
8 - if (y == 0) |
|
9 - y = textArea.getPainter().getLineExtraSpacing(); |
|
10 |
|
11 extensionMgr.paintScreenLineRange(textArea,gfx, |
|
12 firstLine,lastLine,y,lineHeight); |
|
13 @@ -725,7 +723,7 @@ |
|
14 |
|
15 FontMetrics textAreaFm = textArea.getPainter().getFontMetrics(); |
|
16 int lineHeight = textArea.getPainter().getLineHeight(); |
|
17 - int baseline = textAreaFm.getAscent(); |
|
18 + int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent(); |
|
19 |
|
20 ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line); |
|
21 int physicalLine = info.physicalLine; |