# HG changeset patch
# User wenzelm
# Date 1414334762 -3600
# Node ID 11d726ce599ea424c0d42740219039d648481d08
# Parent  c6348a0621311e1cf9ec5c30b422cf3e98594f0f
support negative extraLineSpacing;
updated ErrorList.jar 2.3;

diff -r c6348a062131 -r 11d726ce599e Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sat Oct 25 21:16:32 2014 +0200
+++ b/Admin/components/components.sha1	Sun Oct 26 15:46:02 2014 +0100
@@ -58,6 +58,7 @@
 4a963665537ea66c69de4d761846541ebdbf69f2  jedit_build-20140511.tar.gz
 a9d637a30f6a87a3583f265da51e63e3619cff52  jedit_build-20140722.tar.gz
 f29391c53d85715f8454e1aaa304fbccc352928f  jedit_build-20141018.tar.gz
+d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4  jedit_build-20141026.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 c8a19a36adf6cefa779d85f22ded2f4654e68ea5  jortho-1.0-1.tar.gz
diff -r c6348a062131 -r 11d726ce599e Admin/components/main
--- a/Admin/components/main	Sat Oct 25 21:16:32 2014 +0200
+++ b/Admin/components/main	Sun Oct 26 15:46:02 2014 +0100
@@ -5,7 +5,7 @@
 exec_process-1.0.3
 Haskabelle-2014
 jdk-7u67
-jedit_build-20141018
+jedit_build-20141026
 jfreechart-1.0.14-1
 jortho-1.0-2
 kodkodi-1.5.2
diff -r c6348a062131 -r 11d726ce599e src/Tools/jEdit/patches/structure_matcher
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/structure_matcher	Sun Oct 26 15:46:02 2014 +0100
@@ -0,0 +1,37 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java	2013-07-28 19:03:31.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java	2014-10-26 15:23:15.176502388 +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);
+ 			}
+ 		}
+