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