diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java
--- 5.2.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 2015-02-02 02:14:27.000000000 +0100
+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java 2015-02-28 20:56:32.644328711 +0100
@@ -201,8 +201,9 @@
int matchEndLine = textArea.getScreenLineOfOffset(
match.end);
- int fontHeight = textArea.getPainter().getFontHeight();
- y += textArea.getPainter().getLineExtraSpacing();
+ int height = Math.min(
+ textArea.getPainter().getLineHeight(), textArea.getPainter().getFontHeight());
+ y += Math.max(textArea.getPainter().getLineExtraSpacing(), 0);
int[] offsets = getOffsets(screenLine,match);
int x1 = offsets[0];
@@ -210,8 +211,8 @@
gfx.setColor(textArea.getPainter().getStructureHighlightColor());
- gfx.drawLine(x1,y,x1,y + fontHeight - 1);
- gfx.drawLine(x2,y,x2,y + fontHeight - 1);
+ gfx.drawLine(x1,y,x1,y + height - 1);
+ gfx.drawLine(x2,y,x2,y + height - 1);
if(matchStartLine == screenLine || screenLine == 0)
gfx.drawLine(x1,y,x2,y);
@@ -229,8 +230,8 @@
if(matchEndLine == screenLine)
{
- gfx.drawLine(x1,y + fontHeight - 1,
- x2,y + fontHeight - 1);
+ gfx.drawLine(x1,y + height - 1,
+ x2,y + height - 1);
}
}