updates for jedit-4.5.0 (still inactive);
authorwenzelm
Sun Mar 04 23:04:40 2012 +0100 (2012-03-04)
changeset 4681790c8620852cf
parent 46816 a96b25141220
child 46818 2a28e66e2e4c
updates for jedit-4.5.0 (still inactive);
src/Tools/jEdit/patches/jedit-4.5.0/extended_styles
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/patches/jedit-4.5.0/extended_styles	Sun Mar 04 23:04:40 2012 +0100
     1.3 @@ -0,0 +1,78 @@
     1.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
     1.5 +--- 4.5.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-01-30 23:29:35.000000000 +0100
     1.6 ++++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-03-04 22:14:51.000000000 +0100
     1.7 +@@ -78,7 +78,7 @@
     1.8 + 			start = next;
     1.9 + 			token = token.next;
    1.10 + 		}
    1.11 +-		if (token.id == Token.END || token.id == Token.NULL)
    1.12 ++		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    1.13 + 		{
    1.14 + 			JOptionPane.showMessageDialog(textArea.getView(),
    1.15 + 				jEdit.getProperty("syntax-style-no-token.message"),
    1.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
    1.17 +--- 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-01-30 23:29:42.000000000 +0100
    1.18 ++++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-03-04 22:12:25.000000000 +0100
    1.19 +@@ -380,7 +380,7 @@
    1.20 + 	// this is either style.getBackgroundColor() or
    1.21 + 	// styles[defaultID].getBackgroundColor()
    1.22 + 	private Color background;
    1.23 +-	private String str;
    1.24 ++	public String str;
    1.25 + 	//private GlyphVector gv;
    1.26 + 	private List<GlyphVector> glyphs;
    1.27 + 	private boolean visible;
    1.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
    1.29 +--- 4.5.0/jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-01-30 23:29:42.000000000 +0100
    1.30 ++++ 4.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-03-04 22:15:41.000000000 +0100
    1.31 +@@ -57,7 +57,7 @@
    1.32 + 	 */
    1.33 + 	public static String tokenToString(byte token)
    1.34 + 	{
    1.35 +-		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    1.36 ++		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    1.37 + 	} //}}}
    1.38 + 
    1.39 + 	//{{{ Token types
    1.40 +diff -ru 4.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    1.41 +--- 4.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-01-30 23:29:44.000000000 +0100
    1.42 ++++ 4.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-03-04 22:27:19.000000000 +0100
    1.43 +@@ -194,7 +194,24 @@
    1.44 + 	{
    1.45 + 		return loadStyles(family,size,true);
    1.46 + 	}
    1.47 +-	
    1.48 ++
    1.49 ++	/**
    1.50 ++	 * Extended styles derived from the user-specified style array.
    1.51 ++	 */
    1.52 ++
    1.53 ++	public static class StyleExtender
    1.54 ++	{
    1.55 ++		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    1.56 ++		{
    1.57 ++			return styles;
    1.58 ++		}
    1.59 ++	}
    1.60 ++	volatile private static StyleExtender _styleExtender = new StyleExtender();
    1.61 ++	public static void setStyleExtender(StyleExtender ext)
    1.62 ++	{
    1.63 ++		_styleExtender = ext;
    1.64 ++	}
    1.65 ++
    1.66 + 	/**
    1.67 + 	 * Loads the syntax styles from the properties, giving them the specified
    1.68 + 	 * base font family and size.
    1.69 +@@ -224,9 +241,9 @@
    1.70 + 				Log.log(Log.ERROR,StandardUtilities.class,e);
    1.71 + 			}
    1.72 + 		}
    1.73 +-
    1.74 +-		return styles;
    1.75 ++		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
    1.76 ++		return _styleExtender.extendStyles(styles);
    1.77 + 	} //}}}
    1.78 +-	
    1.79 ++
    1.80 + 	private SyntaxUtilities(){}
    1.81 + }
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sun Mar 04 21:46:22 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sun Mar 04 23:04:40 2012 +0100
     2.3 @@ -182,11 +182,12 @@
     2.4  
     2.5      var result = Map[Text.Offset, Chunk]()
     2.6      for (line <- physical_lines) {
     2.7 +      val line_start = buffer.getLineStartOffset(line)
     2.8 +
     2.9        out.clear
    2.10 -      handler.init(painter.getStyles, font_context, painter, out, margin)
    2.11 +      handler.init(painter.getStyles, font_context, painter, out, margin) // jedit-4.5.0: line_start
    2.12        buffer.markTokens(line, handler)
    2.13  
    2.14 -      val line_start = buffer.getLineStartOffset(line)
    2.15        for (i <- 0 until out.size) {
    2.16          val chunk = out.get(i)
    2.17          result += (line_start + chunk.offset -> chunk)