updated to jedit-4.5.1;
authorwenzelm
Wed Mar 28 00:18:11 2012 +0200 (2012-03-28)
changeset 47158d317a71f24d5
parent 47157 2b0749c80bc8
child 47172 9fc17f9ccd6c
updated to jedit-4.5.1;
NEWS
src/Tools/jEdit/README_BUILD
src/Tools/jEdit/patches/jedit-4.4.1/extended_styles
src/Tools/jEdit/patches/jedit-4.4.1/render_context
src/Tools/jEdit/patches/jedit-4.5.0/extended_styles
src/Tools/jEdit/patches/jedit-4.5.1/extended_styles
     1.1 --- a/NEWS	Tue Mar 27 17:58:53 2012 +0200
     1.2 +++ b/NEWS	Wed Mar 28 00:18:11 2012 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4    - markup for bound variables
     1.5    - markup for types of term variables (e.g. displayed as tooltips)
     1.6    - support for user-defined Isar commands within the running session
     1.7 +  - improved support for Unicode outside original 16bit range
     1.8 +    e.g. glyph for \<A> (thanks to jEdit 4.5.1)
     1.9  
    1.10  * Updated and extended reference manuals ("isar-ref" and
    1.11  "implementation"); reduced remaining material in old "ref" manual.
     2.1 --- a/src/Tools/jEdit/README_BUILD	Tue Mar 27 17:58:53 2012 +0200
     2.2 +++ b/src/Tools/jEdit/README_BUILD	Wed Mar 28 00:18:11 2012 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  * Official Java JDK 1.6 from Sun/Oracle/Apple
     2.5    http://www.oracle.com/technetwork/java/javase/downloads/index.html
     2.6  
     2.7 -  (experimental support for JDK/OpenJDK 1.7)
     2.8 +  (or JDK/OpenJDK 1.7, but not OpenJDK 1.6)
     2.9  
    2.10  * Scala 2.8.2.final or 2.9.1-1
    2.11    http://www.scala-lang.org
    2.12 @@ -12,7 +12,7 @@
    2.13    (experimental support for Scala 2.10.x milestones)
    2.14  
    2.15  * Auxiliary jedit_build component
    2.16 -  http://www4.in.tum.de/~wenzelm/test/jedit_build-20120313.tar.gz
    2.17 +  http://www4.in.tum.de/~wenzelm/test/jedit_build-20120327.tar.gz
    2.18  
    2.19  
    2.20  Important settings within Isabelle environment
     3.1 --- a/src/Tools/jEdit/patches/jedit-4.4.1/extended_styles	Tue Mar 27 17:58:53 2012 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,74 +0,0 @@
     3.4 -diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
     3.5 ---- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-21 01:28:56.000000000 +0200
     3.6 -+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-22 16:07:32.000000000 +0200
     3.7 -@@ -78,7 +78,7 @@
     3.8 - 			start = next;
     3.9 - 			token = token.next;
    3.10 - 		}
    3.11 --		if (token.id == Token.END || token.id == Token.NULL)
    3.12 -+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    3.13 - 		{
    3.14 - 			JOptionPane.showMessageDialog(textArea.getView(),
    3.15 - 				jEdit.getProperty("syntax-style-no-token.message"),
    3.16 -diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
    3.17 ---- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-21 01:29:10.000000000 +0200
    3.18 -+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-22 16:02:07.000000000 +0200
    3.19 -@@ -380,7 +380,7 @@
    3.20 - 	// this is either style.getBackgroundColor() or
    3.21 - 	// styles[defaultID].getBackgroundColor()
    3.22 - 	private Color background;
    3.23 --	private String str;
    3.24 -+	public String str;
    3.25 - 	//private GlyphVector gv;
    3.26 - 	private List<GlyphVector> glyphs;
    3.27 - 	private boolean visible;
    3.28 -diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
    3.29 ---- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2011-06-21 01:29:10.000000000 +0200
    3.30 -+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-22 16:08:47.000000000 +0200
    3.31 -@@ -57,7 +57,7 @@
    3.32 - 	 */
    3.33 - 	public static String tokenToString(byte token)
    3.34 - 	{
    3.35 --		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    3.36 -+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    3.37 - 	} //}}}
    3.38 - 
    3.39 - 	//{{{ Token types
    3.40 -diff -ru 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    3.41 ---- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2011-06-21 01:29:11.000000000 +0200
    3.42 -+++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-22 16:05:28.000000000 +0200
    3.43 -@@ -194,6 +194,23 @@
    3.44 - 	}
    3.45 - 	
    3.46 - 	/**
    3.47 -+	 * Extended styles derived from the user-specified style array.
    3.48 -+	 */
    3.49 -+
    3.50 -+	public static class StyleExtender
    3.51 -+	{
    3.52 -+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    3.53 -+		{
    3.54 -+			return styles;
    3.55 -+		}
    3.56 -+	}
    3.57 -+	volatile private static StyleExtender _styleExtender = new StyleExtender();
    3.58 -+	public static void setStyleExtender(StyleExtender ext)
    3.59 -+	{
    3.60 -+		_styleExtender = ext;
    3.61 -+	}
    3.62 -+
    3.63 -+	/**
    3.64 - 	 * Loads the syntax styles from the properties, giving them the specified
    3.65 - 	 * base font family and size.
    3.66 - 	 * @param family The font family
    3.67 -@@ -222,8 +239,9 @@
    3.68 - 				Log.log(Log.ERROR,StandardUtilities.class,e);
    3.69 - 			}
    3.70 - 		}
    3.71 -+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
    3.72 - 
    3.73 --		return styles;
    3.74 -+		return _styleExtender.extendStyles(styles);
    3.75 - 	} //}}}
    3.76 - 	
    3.77 - 	private SyntaxUtilities(){}
     4.1 --- a/src/Tools/jEdit/patches/jedit-4.4.1/render_context	Tue Mar 27 17:58:53 2012 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,13 +0,0 @@
     4.4 -diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
     4.5 ---- 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-21 01:28:56.000000000 +0200
     4.6 -+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-22 16:18:43.000000000 +0200
     4.7 -@@ -646,7 +646,7 @@
     4.8 - 			this.font = font;
     4.9 - 
    4.10 - 			FontRenderContext fontRenderContext
    4.11 --				= new FontRenderContext(null,true,true);
    4.12 -+				= new FontRenderContext(null,true,false);
    4.13 - 			glyphs = font.createGlyphVector(fontRenderContext,text);
    4.14 - 			width = (int)glyphs.getLogicalBounds().getWidth() + 4;
    4.15 - 			//height = (int)glyphs.getLogicalBounds().getHeight();
    4.16 -
     5.1 --- a/src/Tools/jEdit/patches/jedit-4.5.0/extended_styles	Tue Mar 27 17:58:53 2012 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,78 +0,0 @@
     5.4 -diff -ru 4.5.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.5.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
     5.5 ---- 4.5.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-01-30 23:29:35.000000000 +0100
     5.6 -+++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-04 22:14:51.000000000 +0100
     5.7 -@@ -78,7 +78,7 @@
     5.8 - 			start = next;
     5.9 - 			token = token.next;
    5.10 - 		}
    5.11 --		if (token.id == Token.END || token.id == Token.NULL)
    5.12 -+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    5.13 - 		{
    5.14 - 			JOptionPane.showMessageDialog(textArea.getView(),
    5.15 - 				jEdit.getProperty("syntax-style-no-token.message"),
    5.16 -diff -ru 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
    5.17 ---- 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-01-30 23:29:42.000000000 +0100
    5.18 -+++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-04 22:12:25.000000000 +0100
    5.19 -@@ -380,7 +380,7 @@
    5.20 - 	// this is either style.getBackgroundColor() or
    5.21 - 	// styles[defaultID].getBackgroundColor()
    5.22 - 	private Color background;
    5.23 --	private String str;
    5.24 -+	public String str;
    5.25 - 	//private GlyphVector gv;
    5.26 - 	private List<GlyphVector> glyphs;
    5.27 - 	private boolean visible;
    5.28 -diff -ru 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
    5.29 ---- 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-01-30 23:29:42.000000000 +0100
    5.30 -+++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-03-04 22:15:41.000000000 +0100
    5.31 -@@ -57,7 +57,7 @@
    5.32 - 	 */
    5.33 - 	public static String tokenToString(byte token)
    5.34 - 	{
    5.35 --		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    5.36 -+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    5.37 - 	} //}}}
    5.38 - 
    5.39 - 	//{{{ Token types
    5.40 -diff -ru 4.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    5.41 ---- 4.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-01-30 23:29:44.000000000 +0100
    5.42 -+++ 4.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-03-04 22:27:19.000000000 +0100
    5.43 -@@ -194,7 +194,24 @@
    5.44 - 	{
    5.45 - 		return loadStyles(family,size,true);
    5.46 - 	}
    5.47 --	
    5.48 -+
    5.49 -+	/**
    5.50 -+	 * Extended styles derived from the user-specified style array.
    5.51 -+	 */
    5.52 -+
    5.53 -+	public static class StyleExtender
    5.54 -+	{
    5.55 -+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    5.56 -+		{
    5.57 -+			return styles;
    5.58 -+		}
    5.59 -+	}
    5.60 -+	volatile private static StyleExtender _styleExtender = new StyleExtender();
    5.61 -+	public static void setStyleExtender(StyleExtender ext)
    5.62 -+	{
    5.63 -+		_styleExtender = ext;
    5.64 -+	}
    5.65 -+
    5.66 - 	/**
    5.67 - 	 * Loads the syntax styles from the properties, giving them the specified
    5.68 - 	 * base font family and size.
    5.69 -@@ -224,9 +241,9 @@
    5.70 - 				Log.log(Log.ERROR,StandardUtilities.class,e);
    5.71 - 			}
    5.72 - 		}
    5.73 --
    5.74 --		return styles;
    5.75 -+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
    5.76 -+		return _styleExtender.extendStyles(styles);
    5.77 - 	} //}}}
    5.78 --	
    5.79 -+
    5.80 - 	private SyntaxUtilities(){}
    5.81 - }
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/jEdit/patches/jedit-4.5.1/extended_styles	Wed Mar 28 00:18:11 2012 +0200
     6.3 @@ -0,0 +1,78 @@
     6.4 +diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
     6.5 +--- 4.5.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-25 18:51:52.000000000 +0200
     6.6 ++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-27 23:30:26.000000000 +0200
     6.7 +@@ -78,7 +78,7 @@
     6.8 + 			start = next;
     6.9 + 			token = token.next;
    6.10 + 		}
    6.11 +-		if (token.id == Token.END || token.id == Token.NULL)
    6.12 ++		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    6.13 + 		{
    6.14 + 			JOptionPane.showMessageDialog(textArea.getView(),
    6.15 + 				jEdit.getProperty("syntax-style-no-token.message"),
    6.16 +diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
    6.17 +--- 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-25 18:52:01.000000000 +0200
    6.18 ++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-27 23:31:27.000000000 +0200
    6.19 +@@ -380,7 +380,7 @@
    6.20 + 	// this is either style.getBackgroundColor() or
    6.21 + 	// styles[defaultID].getBackgroundColor()
    6.22 + 	private Color background;
    6.23 +-	private String str;
    6.24 ++	public String str;
    6.25 + 	//private GlyphVector gv;
    6.26 + 	private List<GlyphVector> glyphs;
    6.27 + 	private boolean visible;
    6.28 +diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
    6.29 +--- 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-03-25 18:52:01.000000000 +0200
    6.30 ++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-03-27 23:30:57.000000000 +0200
    6.31 +@@ -57,7 +57,7 @@
    6.32 + 	 */
    6.33 + 	public static String tokenToString(byte token)
    6.34 + 	{
    6.35 +-		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    6.36 ++		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    6.37 + 	} //}}}
    6.38 + 
    6.39 + 	//{{{ Token types
    6.40 +diff -ru 4.5.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.5.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    6.41 +--- 4.5.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-03-25 18:52:03.000000000 +0200
    6.42 ++++ 4.5.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-03-27 23:33:07.000000000 +0200
    6.43 +@@ -194,7 +194,24 @@
    6.44 + 	{
    6.45 + 		return loadStyles(family,size,true);
    6.46 + 	}
    6.47 +-	
    6.48 ++
    6.49 ++	/**
    6.50 ++	 * Extended styles derived from the user-specified style array.
    6.51 ++	 */
    6.52 ++
    6.53 ++	public static class StyleExtender
    6.54 ++	{
    6.55 ++		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    6.56 ++		{
    6.57 ++			return styles;
    6.58 ++		}
    6.59 ++	}
    6.60 ++	volatile private static StyleExtender _styleExtender = new StyleExtender();
    6.61 ++	public static void setStyleExtender(StyleExtender ext)
    6.62 ++	{
    6.63 ++		_styleExtender = ext;
    6.64 ++	}
    6.65 ++
    6.66 + 	/**
    6.67 + 	 * Loads the syntax styles from the properties, giving them the specified
    6.68 + 	 * base font family and size.
    6.69 +@@ -224,9 +241,9 @@
    6.70 + 				Log.log(Log.ERROR,StandardUtilities.class,e);
    6.71 + 			}
    6.72 + 		}
    6.73 +-
    6.74 +-		return styles;
    6.75 ++		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
    6.76 ++		return _styleExtender.extendStyles(styles);
    6.77 + 	} //}}}
    6.78 +-	
    6.79 ++
    6.80 + 	private SyntaxUtilities(){}
    6.81 + }