src/Tools/jEdit/patches/structure_matcher

predicate compiler: ignore Abs_filter and Rep_filter

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);
 			}
 		}