diff -r 6bccb1dc9bc3 -r a96b25141220 src/Tools/jEdit/patches/jedit-4.4.1/extended_styles --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/jedit-4.4.1/extended_styles Sun Mar 04 21:46:22 2012 +0100 @@ -0,0 +1,74 @@ +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 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(){}