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);
authorwenzelm
Tue, 24 Nov 2015 22:50:03 +0100
changeset 61746 3df1b6a5837c
parent 61745 e23e0ff98657
child 61747 a870098fc27e
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;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/patches/brackets_extended_styles
src/Tools/jEdit/patches/gutter
src/Tools/jEdit/src/Isabelle.props
--- 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