paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
avoid hardwired colors (see 1d9c121cbe4d);
updated to Highlight 2.2;
--- a/Admin/components/components.sha1 Tue Nov 24 10:54:21 2015 +0100
+++ b/Admin/components/components.sha1 Tue Nov 24 22:50:03 2015 +0100
@@ -79,6 +79,7 @@
f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz
14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.tar.gz
b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz
+8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.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 Tue Nov 24 10:54:21 2015 +0100
+++ b/Admin/components/main Tue Nov 24 22:50:03 2015 +0100
@@ -6,7 +6,7 @@
Haskabelle-2015
isabelle_fonts-20151107
jdk-8u66
-jedit_build-20151023
+jedit_build-20151124
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
--- a/src/Tools/jEdit/patches/brackets_extended_styles Tue Nov 24 10:54:21 2015 +0100
+++ b/src/Tools/jEdit/patches/brackets_extended_styles Tue Nov 24 22:50:03 2015 +0100
@@ -98,9 +98,9 @@
default: return '\0';
}
} //}}}
-diff -ru 5.3.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.3.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2015-10-20 19:56:08.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-10-23 20:02:22.161225360 +0200
+diff -ru 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2015-10-20 19:56:08.000000000 +0200
++++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-11-24 22:14:56.935661997 +0100
@@ -194,7 +194,24 @@
{
return loadStyles(family,size,true);
@@ -127,13 +127,15 @@
/**
* Loads the syntax styles from the properties, giving them the specified
* base font family and size.
-@@ -224,9 +241,9 @@
+@@ -224,9 +241,11 @@
Log.log(Log.ERROR,StandardUtilities.class,e);
}
}
-
- return styles;
-+ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
++ styles[0] =
++ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
++ null, new Font(family, 0, size));
+ return _styleExtender.extendStyles(styles);
} //}}}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/gutter Tue Nov 24 22:50:03 2015 +0100
@@ -0,0 +1,21 @@
+diff -ru 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java
+--- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 2015-10-20 19:56:03.000000000 +0200
++++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java 2015-11-24 21:58:47.686343684 +0100
+@@ -185,8 +185,6 @@
+ }
+
+ int y = clip.y - clip.y % lineHeight;
+- if (y == 0)
+- y = textArea.getPainter().getLineExtraSpacing();
+
+ extensionMgr.paintScreenLineRange(textArea,gfx,
+ firstLine,lastLine,y,lineHeight);
+@@ -725,7 +723,7 @@
+
+ FontMetrics textAreaFm = textArea.getPainter().getFontMetrics();
+ int lineHeight = textArea.getPainter().getLineHeight();
+- int baseline = textAreaFm.getAscent();
++ int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent();
+
+ ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line);
+ int physicalLine = info.physicalLine;
--- a/src/Tools/jEdit/src/Isabelle.props Tue Nov 24 10:54:21 2015 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Nov 24 22:50:03 2015 +0100
@@ -18,7 +18,7 @@
plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
-plugin.isabelle.jedit.Plugin.depend.5=plugin gatchan.highlight.HighlightPlugin 2.0
+plugin.isabelle.jedit.Plugin.depend.5=plugin gatchan.highlight.HighlightPlugin 2.2
#options
plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering