# HG changeset patch
# User wenzelm
# Date 1448401803 -3600
# Node ID 3df1b6a5837c74105d03800d7c470e337de3d0a6
# Parent  e23e0ff98657145ef96b6c971bc6fda93b904698
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;

diff -r e23e0ff98657 -r 3df1b6a5837c Admin/components/components.sha1
--- 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
diff -r e23e0ff98657 -r 3df1b6a5837c Admin/components/main
--- 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
diff -r e23e0ff98657 -r 3df1b6a5837c src/Tools/jEdit/patches/brackets_extended_styles
--- 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);
  	} //}}}
 -	
diff -r e23e0ff98657 -r 3df1b6a5837c src/Tools/jEdit/patches/gutter
--- /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;
diff -r e23e0ff98657 -r 3df1b6a5837c src/Tools/jEdit/src/Isabelle.props
--- 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