--- a/src/Tools/jEdit/patches/structure_matcher Fri Oct 23 18:39:14 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-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);
- }
- }
-