# HG changeset patch
# User wenzelm
# Date 1332886691 -7200
# Node ID d317a71f24d5fa51c80bf66fdbd4c9d847fa58fe
# Parent  2b0749c80bc867bf8b450c16e36abf3d053e7855
updated to jedit-4.5.1;

diff -r 2b0749c80bc8 -r d317a71f24d5 NEWS
--- a/NEWS	Tue Mar 27 17:58:53 2012 +0200
+++ b/NEWS	Wed Mar 28 00:18:11 2012 +0200
@@ -11,6 +11,8 @@
   - markup for bound variables
   - markup for types of term variables (e.g. displayed as tooltips)
   - support for user-defined Isar commands within the running session
+  - improved support for Unicode outside original 16bit range
+    e.g. glyph for \<A> (thanks to jEdit 4.5.1)
 
 * Updated and extended reference manuals ("isar-ref" and
 "implementation"); reduced remaining material in old "ref" manual.
diff -r 2b0749c80bc8 -r d317a71f24d5 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Tue Mar 27 17:58:53 2012 +0200
+++ b/src/Tools/jEdit/README_BUILD	Wed Mar 28 00:18:11 2012 +0200
@@ -4,7 +4,7 @@
 * Official Java JDK 1.6 from Sun/Oracle/Apple
   http://www.oracle.com/technetwork/java/javase/downloads/index.html
 
-  (experimental support for JDK/OpenJDK 1.7)
+  (or JDK/OpenJDK 1.7, but not OpenJDK 1.6)
 
 * Scala 2.8.2.final or 2.9.1-1
   http://www.scala-lang.org
@@ -12,7 +12,7 @@
   (experimental support for Scala 2.10.x milestones)
 
 * Auxiliary jedit_build component
-  http://www4.in.tum.de/~wenzelm/test/jedit_build-20120313.tar.gz
+  http://www4.in.tum.de/~wenzelm/test/jedit_build-20120327.tar.gz
 
 
 Important settings within Isabelle environment
diff -r 2b0749c80bc8 -r d317a71f24d5 src/Tools/jEdit/patches/jedit-4.4.1/extended_styles
--- a/src/Tools/jEdit/patches/jedit-4.4.1/extended_styles	Tue Mar 27 17:58:53 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-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
---- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-21 01:28:56.000000000 +0200
-+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-22 16:07:32.000000000 +0200
-@@ -78,7 +78,7 @@
- 			start = next;
- 			token = token.next;
- 		}
--		if (token.id == Token.END || token.id == Token.NULL)
-+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
- 		{
- 			JOptionPane.showMessageDialog(textArea.getView(),
- 				jEdit.getProperty("syntax-style-no-token.message"),
-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
---- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-21 01:29:10.000000000 +0200
-+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-22 16:02:07.000000000 +0200
-@@ -380,7 +380,7 @@
- 	// this is either style.getBackgroundColor() or
- 	// styles[defaultID].getBackgroundColor()
- 	private Color background;
--	private String str;
-+	public String str;
- 	//private GlyphVector gv;
- 	private List<GlyphVector> glyphs;
- 	private boolean visible;
-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
---- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2011-06-21 01:29:10.000000000 +0200
-+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-22 16:08:47.000000000 +0200
-@@ -57,7 +57,7 @@
- 	 */
- 	public static String tokenToString(byte token)
- 	{
--		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
-+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
- 	} //}}}
- 
- 	//{{{ Token types
-diff -ru 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2011-06-21 01:29:11.000000000 +0200
-+++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-22 16:05:28.000000000 +0200
-@@ -194,6 +194,23 @@
- 	}
- 	
- 	/**
-+	 * Extended styles derived from the user-specified style array.
-+	 */
-+
-+	public static class StyleExtender
-+	{
-+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
-+		{
-+			return styles;
-+		}
-+	}
-+	volatile private static StyleExtender _styleExtender = new StyleExtender();
-+	public static void setStyleExtender(StyleExtender ext)
-+	{
-+		_styleExtender = ext;
-+	}
-+
-+	/**
- 	 * Loads the syntax styles from the properties, giving them the specified
- 	 * base font family and size.
- 	 * @param family The font family
-@@ -222,8 +239,9 @@
- 				Log.log(Log.ERROR,StandardUtilities.class,e);
- 			}
- 		}
-+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
- 
--		return styles;
-+		return _styleExtender.extendStyles(styles);
- 	} //}}}
- 	
- 	private SyntaxUtilities(){}
diff -r 2b0749c80bc8 -r d317a71f24d5 src/Tools/jEdit/patches/jedit-4.4.1/render_context
--- a/src/Tools/jEdit/patches/jedit-4.4.1/render_context	Tue Mar 27 17:58:53 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-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.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-21 01:28:56.000000000 +0200
-+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-22 16:18:43.000000000 +0200
-@@ -646,7 +646,7 @@
- 			this.font = font;
- 
- 			FontRenderContext fontRenderContext
--				= new FontRenderContext(null,true,true);
-+				= new FontRenderContext(null,true,false);
- 			glyphs = font.createGlyphVector(fontRenderContext,text);
- 			width = (int)glyphs.getLogicalBounds().getWidth() + 4;
- 			//height = (int)glyphs.getLogicalBounds().getHeight();
-
diff -r 2b0749c80bc8 -r d317a71f24d5 src/Tools/jEdit/patches/jedit-4.5.0/extended_styles
--- a/src/Tools/jEdit/patches/jedit-4.5.0/extended_styles	Tue Mar 27 17:58:53 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-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
---- 4.5.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-01-30 23:29:35.000000000 +0100
-+++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-04 22:14:51.000000000 +0100
-@@ -78,7 +78,7 @@
- 			start = next;
- 			token = token.next;
- 		}
--		if (token.id == Token.END || token.id == Token.NULL)
-+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
- 		{
- 			JOptionPane.showMessageDialog(textArea.getView(),
- 				jEdit.getProperty("syntax-style-no-token.message"),
-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
---- 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-01-30 23:29:42.000000000 +0100
-+++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-04 22:12:25.000000000 +0100
-@@ -380,7 +380,7 @@
- 	// this is either style.getBackgroundColor() or
- 	// styles[defaultID].getBackgroundColor()
- 	private Color background;
--	private String str;
-+	public String str;
- 	//private GlyphVector gv;
- 	private List<GlyphVector> glyphs;
- 	private boolean visible;
-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
---- 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-01-30 23:29:42.000000000 +0100
-+++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-03-04 22:15:41.000000000 +0100
-@@ -57,7 +57,7 @@
- 	 */
- 	public static String tokenToString(byte token)
- 	{
--		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
-+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
- 	} //}}}
- 
- 	//{{{ Token types
-diff -ru 4.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 4.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-01-30 23:29:44.000000000 +0100
-+++ 4.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-03-04 22:27:19.000000000 +0100
-@@ -194,7 +194,24 @@
- 	{
- 		return loadStyles(family,size,true);
- 	}
--	
-+
-+	/**
-+	 * Extended styles derived from the user-specified style array.
-+	 */
-+
-+	public static class StyleExtender
-+	{
-+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
-+		{
-+			return styles;
-+		}
-+	}
-+	volatile private static StyleExtender _styleExtender = new StyleExtender();
-+	public static void setStyleExtender(StyleExtender ext)
-+	{
-+		_styleExtender = ext;
-+	}
-+
- 	/**
- 	 * Loads the syntax styles from the properties, giving them the specified
- 	 * base font family and size.
-@@ -224,9 +241,9 @@
- 				Log.log(Log.ERROR,StandardUtilities.class,e);
- 			}
- 		}
--
--		return styles;
-+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
-+		return _styleExtender.extendStyles(styles);
- 	} //}}}
--	
-+
- 	private SyntaxUtilities(){}
- }
diff -r 2b0749c80bc8 -r d317a71f24d5 src/Tools/jEdit/patches/jedit-4.5.1/extended_styles
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit-4.5.1/extended_styles	Wed Mar 28 00:18:11 2012 +0200
@@ -0,0 +1,78 @@
+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
+--- 4.5.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-25 18:51:52.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-27 23:30:26.000000000 +0200
+@@ -78,7 +78,7 @@
+ 			start = next;
+ 			token = token.next;
+ 		}
+-		if (token.id == Token.END || token.id == Token.NULL)
++		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
+ 		{
+ 			JOptionPane.showMessageDialog(textArea.getView(),
+ 				jEdit.getProperty("syntax-style-no-token.message"),
+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
+--- 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-25 18:52:01.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-27 23:31:27.000000000 +0200
+@@ -380,7 +380,7 @@
+ 	// this is either style.getBackgroundColor() or
+ 	// styles[defaultID].getBackgroundColor()
+ 	private Color background;
+-	private String str;
++	public String str;
+ 	//private GlyphVector gv;
+ 	private List<GlyphVector> glyphs;
+ 	private boolean visible;
+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
+--- 4.5.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-03-25 18:52:01.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-03-27 23:30:57.000000000 +0200
+@@ -57,7 +57,7 @@
+ 	 */
+ 	public static String tokenToString(byte token)
+ 	{
+-		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
++		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
+ 	} //}}}
+ 
+ 	//{{{ Token types
+diff -ru 4.5.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.5.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 4.5.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-03-25 18:52:03.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-03-27 23:33:07.000000000 +0200
+@@ -194,7 +194,24 @@
+ 	{
+ 		return loadStyles(family,size,true);
+ 	}
+-	
++
++	/**
++	 * Extended styles derived from the user-specified style array.
++	 */
++
++	public static class StyleExtender
++	{
++		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
++		{
++			return styles;
++		}
++	}
++	volatile private static StyleExtender _styleExtender = new StyleExtender();
++	public static void setStyleExtender(StyleExtender ext)
++	{
++		_styleExtender = ext;
++	}
++
+ 	/**
+ 	 * Loads the syntax styles from the properties, giving them the specified
+ 	 * base font family and size.
+@@ -224,9 +241,9 @@
+ 				Log.log(Log.ERROR,StandardUtilities.class,e);
+ 			}
+ 		}
+-
+-		return styles;
++		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
++		return _styleExtender.extendStyles(styles);
+ 	} //}}}
+-	
++
+ 	private SyntaxUtilities(){}
+ }