# HG changeset patch
# User wenzelm
# Date 1308753156 -7200
# Node ID bf7400573617fe27f0c2faea91eb28ce4215737c
# Parent  0aca4edbfa99ee59ad7e7b11fd25dc3b340a253d
updated to jedit-4.4.1 and jedit_build-20110622;

diff -r 0aca4edbfa99 -r bf7400573617 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Jun 22 16:01:30 2011 +0200
+++ b/Admin/isatest/isatest-makedist	Wed Jun 22 16:32:36 2011 +0200
@@ -59,7 +59,7 @@
 
 echo "### building distribution"  >> $DISTLOG 2>&1
 mkdir -p $DISTPREFIX
-$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110620" >> $DISTLOG 2>&1
+$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110622" >> $DISTLOG 2>&1
 
 if [ $? -ne 0 ]
 then
diff -r 0aca4edbfa99 -r bf7400573617 src/Tools/jEdit/patches/extended_styles
--- a/src/Tools/jEdit/patches/extended_styles	Wed Jun 22 16:01:30 2011 +0200
+++ b/src/Tools/jEdit/patches/extended_styles	Wed Jun 22 16:32:36 2011 +0200
@@ -1,63 +1,74 @@
-Only in jEdit-patched: build
-diff -ru jEdit/org/gjt/sp/jedit/Buffer.java jEdit-patched/org/gjt/sp/jedit/Buffer.java
---- jEdit/org/gjt/sp/jedit/Buffer.java	2010-05-09 14:29:25.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/Buffer.java	2011-06-18 18:28:19.000000000 +0200
-@@ -2232,7 +2232,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(jEdit.getActiveView(),
- 				jEdit.getProperty("syntax-style-no-token.message"),
-diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
---- jEdit/org/gjt/sp/jedit/syntax/Token.java	2010-05-09 14:29:24.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-18 18:28:10.000000000 +0200
+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 jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- jEdit/org/gjt/sp/util/SyntaxUtilities.java	2010-05-09 14:29:29.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-20 21:30:58.000000000 +0200
+ 	 */
+ 	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
+ 	}
+ 	
+ 	/**
++	 * 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(){}
+ 				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 0aca4edbfa99 -r bf7400573617 src/Tools/jEdit/patches/render_context
--- a/src/Tools/jEdit/patches/render_context	Wed Jun 22 16:01:30 2011 +0200
+++ b/src/Tools/jEdit/patches/render_context	Wed Jun 22 16:32:36 2011 +0200
@@ -1,6 +1,6 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2010-05-09 14:29:17.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-21 23:00:11.000000000 +0200
+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;
  
@@ -10,3 +10,4 @@
  			glyphs = font.createGlyphVector(fontRenderContext,text);
  			width = (int)glyphs.getLogicalBounds().getWidth() + 4;
  			//height = (int)glyphs.getLogicalBounds().getHeight();
+
diff -r 0aca4edbfa99 -r bf7400573617 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:01:30 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:32:36 2011 +0200
@@ -198,8 +198,7 @@
     while (chunk != null) {
       val chunk_offset = line_start + chunk.offset
       if (x + w + chunk.width > clip_rect.x &&
-          x + w < clip_rect.x + clip_rect.width &&
-          chunk.accessable && chunk.visible)
+          x + w < clip_rect.x + clip_rect.width && chunk.accessable)
       {
         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
         val chunk_font = chunk.style.getFont