--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/extended_styles Wed Sep 25 20:29:28 2013 +0200
@@ -0,0 +1,105 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2013-07-28 19:03:38.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2013-09-05 10:51:29.192192327 +0200
+@@ -79,7 +79,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 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2013-07-28 19:03:51.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2013-09-05 10:51:29.192192327 +0200
+@@ -256,9 +256,9 @@
+ //{{{ Package private members
+
+ //{{{ Instance variables
+- SyntaxStyle style;
++ public SyntaxStyle style;
+ // set up after init()
+- float width;
++ public float width;
+ //}}}
+
+ //{{{ Chunk constructor
+@@ -506,7 +506,7 @@
+ // this is either style.getBackgroundColor() or
+ // styles[defaultID].getBackgroundColor()
+ private Color background;
+- private String str;
++ public String str;
+ private GlyphVector[] glyphs;
+ //}}}
+
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2013-07-28 19:03:51.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2013-09-05 10:51:29.192192327 +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 5.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2013-07-28 19:03:53.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2013-09-05 10:51:29.192192327 +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(){}
+ }
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2013-07-28 19:03:32.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2013-09-05 10:51:29.196192309 +0200
+@@ -907,6 +907,11 @@
+ return chunkCache.getLineInfo(screenLine).physicalLine;
+ } //}}}
+
++ public Chunk getChunksOfScreenLine(int screenLine)
++ {
++ return chunkCache.getLineInfo(screenLine).chunks;
++ }
++
+ //{{{ getScreenLineOfOffset() method
+ /**
+ * Returns the screen (wrapped) line containing the specified offset.