paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
avoid hardwired colors (see 1d9c121cbe4d);
updated to Highlight 2.2;
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
--- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 2015-10-20 19:56:03.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java 2015-11-24 21:58:47.686343684 +0100
@@ -185,8 +185,6 @@
}
int y = clip.y - clip.y % lineHeight;
- if (y == 0)
- y = textArea.getPainter().getLineExtraSpacing();
extensionMgr.paintScreenLineRange(textArea,gfx,
firstLine,lastLine,y,lineHeight);
@@ -725,7 +723,7 @@
FontMetrics textAreaFm = textArea.getPainter().getFontMetrics();
int lineHeight = textArea.getPainter().getLineHeight();
- int baseline = textAreaFm.getAscent();
+ int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent();
ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line);
int physicalLine = info.physicalLine;