updated to jedit-4.4.1 and jedit_build-20110622;
authorwenzelm
Wed Jun 22 16:32:36 2011 +0200 (2011-06-22)
changeset 43506bf7400573617
parent 43505 0aca4edbfa99
child 43508 bbbd6cad7df1
updated to jedit-4.4.1 and jedit_build-20110622;
Admin/isatest/isatest-makedist
src/Tools/jEdit/patches/extended_styles
src/Tools/jEdit/patches/render_context
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/Admin/isatest/isatest-makedist	Wed Jun 22 16:01:30 2011 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Wed Jun 22 16:32:36 2011 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4  
     1.5  echo "### building distribution"  >> $DISTLOG 2>&1
     1.6  mkdir -p $DISTPREFIX
     1.7 -$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110620" >> $DISTLOG 2>&1
     1.8 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110622" >> $DISTLOG 2>&1
     1.9  
    1.10  if [ $? -ne 0 ]
    1.11  then
     2.1 --- a/src/Tools/jEdit/patches/extended_styles	Wed Jun 22 16:01:30 2011 +0200
     2.2 +++ b/src/Tools/jEdit/patches/extended_styles	Wed Jun 22 16:32:36 2011 +0200
     2.3 @@ -1,63 +1,74 @@
     2.4 -Only in jEdit-patched: build
     2.5 -diff -ru jEdit/org/gjt/sp/jedit/Buffer.java jEdit-patched/org/gjt/sp/jedit/Buffer.java
     2.6 ---- jEdit/org/gjt/sp/jedit/Buffer.java	2010-05-09 14:29:25.000000000 +0200
     2.7 -+++ jEdit-patched/org/gjt/sp/jedit/Buffer.java	2011-06-18 18:28:19.000000000 +0200
     2.8 -@@ -2232,7 +2232,7 @@
     2.9 - 			start = next;
    2.10 - 			token = token.next;
    2.11 - 		}
    2.12 --		if (token.id == Token.END || token.id == Token.NULL)
    2.13 -+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    2.14 - 		{
    2.15 - 			JOptionPane.showMessageDialog(jEdit.getActiveView(),
    2.16 - 				jEdit.getProperty("syntax-style-no-token.message"),
    2.17 -diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
    2.18 ---- jEdit/org/gjt/sp/jedit/syntax/Token.java	2010-05-09 14:29:24.000000000 +0200
    2.19 -+++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-18 18:28:10.000000000 +0200
    2.20 +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
    2.21 +--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-21 01:28:56.000000000 +0200
    2.22 ++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-22 16:07:32.000000000 +0200
    2.23 +@@ -78,7 +78,7 @@
    2.24 + 			start = next;
    2.25 + 			token = token.next;
    2.26 + 		}
    2.27 +-		if (token.id == Token.END || token.id == Token.NULL)
    2.28 ++		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    2.29 + 		{
    2.30 + 			JOptionPane.showMessageDialog(textArea.getView(),
    2.31 + 				jEdit.getProperty("syntax-style-no-token.message"),
    2.32 +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
    2.33 +--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-21 01:29:10.000000000 +0200
    2.34 ++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-22 16:02:07.000000000 +0200
    2.35 +@@ -380,7 +380,7 @@
    2.36 + 	// this is either style.getBackgroundColor() or
    2.37 + 	// styles[defaultID].getBackgroundColor()
    2.38 + 	private Color background;
    2.39 +-	private String str;
    2.40 ++	public String str;
    2.41 + 	//private GlyphVector gv;
    2.42 + 	private List<GlyphVector> glyphs;
    2.43 + 	private boolean visible;
    2.44 +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
    2.45 +--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2011-06-21 01:29:10.000000000 +0200
    2.46 ++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-22 16:08:47.000000000 +0200
    2.47  @@ -57,7 +57,7 @@
    2.48 - 	 */
    2.49 - 	public static String tokenToString(byte token)
    2.50 - 	{
    2.51 --		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    2.52 -+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    2.53 - 	} //}}}
    2.54 - 
    2.55 - 	//{{{ Token types
    2.56 -diff -ru jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    2.57 ---- jEdit/org/gjt/sp/util/SyntaxUtilities.java	2010-05-09 14:29:29.000000000 +0200
    2.58 -+++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-20 21:30:58.000000000 +0200
    2.59 + 	 */
    2.60 + 	public static String tokenToString(byte token)
    2.61 + 	{
    2.62 +-		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    2.63 ++		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    2.64 + 	} //}}}
    2.65 + 
    2.66 + 	//{{{ Token types
    2.67 +diff -ru 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    2.68 +--- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2011-06-21 01:29:11.000000000 +0200
    2.69 ++++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-22 16:05:28.000000000 +0200
    2.70  @@ -194,6 +194,23 @@
    2.71 - 	}
    2.72 - 	
    2.73 - 	/**
    2.74 -+	 * Extended styles derived from the user-specified style array.
    2.75 -+	 */
    2.76 -+
    2.77 -+	public static class StyleExtender
    2.78 -+	{
    2.79 -+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    2.80 -+		{
    2.81 -+			return styles;
    2.82 -+		}
    2.83 -+	}
    2.84 -+	volatile private static StyleExtender _styleExtender = new StyleExtender();
    2.85 -+	public static void setStyleExtender(StyleExtender ext)
    2.86 -+	{
    2.87 -+		_styleExtender = ext;
    2.88 -+	}
    2.89 -+
    2.90 -+	/**
    2.91 - 	 * Loads the syntax styles from the properties, giving them the specified
    2.92 - 	 * base font family and size.
    2.93 - 	 * @param family The font family
    2.94 + 	}
    2.95 + 	
    2.96 + 	/**
    2.97 ++	 * Extended styles derived from the user-specified style array.
    2.98 ++	 */
    2.99 ++
   2.100 ++	public static class StyleExtender
   2.101 ++	{
   2.102 ++		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
   2.103 ++		{
   2.104 ++			return styles;
   2.105 ++		}
   2.106 ++	}
   2.107 ++	volatile private static StyleExtender _styleExtender = new StyleExtender();
   2.108 ++	public static void setStyleExtender(StyleExtender ext)
   2.109 ++	{
   2.110 ++		_styleExtender = ext;
   2.111 ++	}
   2.112 ++
   2.113 ++	/**
   2.114 + 	 * Loads the syntax styles from the properties, giving them the specified
   2.115 + 	 * base font family and size.
   2.116 + 	 * @param family The font family
   2.117  @@ -222,8 +239,9 @@
   2.118 - 				Log.log(Log.ERROR,StandardUtilities.class,e);
   2.119 - 			}
   2.120 - 		}
   2.121 -+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
   2.122 - 
   2.123 --		return styles;
   2.124 -+		return _styleExtender.extendStyles(styles);
   2.125 - 	} //}}}
   2.126 - 	
   2.127 - 	private SyntaxUtilities(){}
   2.128 + 				Log.log(Log.ERROR,StandardUtilities.class,e);
   2.129 + 			}
   2.130 + 		}
   2.131 ++		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
   2.132 + 
   2.133 +-		return styles;
   2.134 ++		return _styleExtender.extendStyles(styles);
   2.135 + 	} //}}}
   2.136 + 	
   2.137 + 	private SyntaxUtilities(){}
     3.1 --- a/src/Tools/jEdit/patches/render_context	Wed Jun 22 16:01:30 2011 +0200
     3.2 +++ b/src/Tools/jEdit/patches/render_context	Wed Jun 22 16:32:36 2011 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4 -diff -ru jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
     3.5 ---- jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2010-05-09 14:29:17.000000000 +0200
     3.6 -+++ jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-21 23:00:11.000000000 +0200
     3.7 +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
     3.8 +--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-21 01:28:56.000000000 +0200
     3.9 ++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2011-06-22 16:18:43.000000000 +0200
    3.10  @@ -646,7 +646,7 @@
    3.11   			this.font = font;
    3.12   
    3.13 @@ -10,3 +10,4 @@
    3.14   			glyphs = font.createGlyphVector(fontRenderContext,text);
    3.15   			width = (int)glyphs.getLogicalBounds().getWidth() + 4;
    3.16   			//height = (int)glyphs.getLogicalBounds().getHeight();
    3.17 +
     4.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:01:30 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:32:36 2011 +0200
     4.3 @@ -198,8 +198,7 @@
     4.4      while (chunk != null) {
     4.5        val chunk_offset = line_start + chunk.offset
     4.6        if (x + w + chunk.width > clip_rect.x &&
     4.7 -          x + w < clip_rect.x + clip_rect.width &&
     4.8 -          chunk.accessable && chunk.visible)
     4.9 +          x + w < clip_rect.x + clip_rect.width && chunk.accessable)
    4.10        {
    4.11          val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
    4.12          val chunk_font = chunk.style.getFont