diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
--- 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2015-10-20 19:56:05.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2015-10-23 20:02:22.161225360 +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.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
--- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2015-10-20 19:56:07.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2015-10-23 20:02:22.161225360 +0200
@@ -259,9 +259,9 @@
//{{{ Package private members
//{{{ Instance variables
- SyntaxStyle style;
+ public SyntaxStyle style;
// set up after init()
- float width;
+ public float width;
//}}}
//{{{ Chunk constructor
@@ -509,7 +509,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.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
--- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2015-10-20 19:56:07.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2015-10-23 20:02:22.161225360 +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.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
--- 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2015-10-20 19:56:03.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2015-10-23 20:02:22.161225360 +0200
@@ -910,6 +910,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.
@@ -1618,8 +1623,8 @@
}
// Scan backwards, trying to find a bracket
- String openBrackets = "([{";
- String closeBrackets = ")]}";
+ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
+ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
int count = 1;
char openBracket = '\0';
char closeBracket = '\0';
diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
--- 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2015-10-20 19:56:00.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2015-10-23 19:46:33.728522904 +0200
@@ -97,6 +97,22 @@
case '}': if (direction != null) direction[0] = false; return '{';
case '<': if (direction != null) direction[0] = true; return '>';
case '>': if (direction != null) direction[0] = false; return '<';
+ case '«': if (direction != null) direction[0] = true; return '»';
+ case '»': if (direction != null) direction[0] = false; return '«';
+ case '‹': if (direction != null) direction[0] = true; return '›';
+ case '›': if (direction != null) direction[0] = false; return '‹';
+ case '⟨': if (direction != null) direction[0] = true; return '⟩';
+ case '⟩': if (direction != null) direction[0] = false; return '⟨';
+ case '⌈': if (direction != null) direction[0] = true; return '⌉';
+ case '⌉': if (direction != null) direction[0] = false; return '⌈';
+ case '⌊': if (direction != null) direction[0] = true; return '⌋';
+ case '⌋': if (direction != null) direction[0] = false; return '⌊';
+ case '⦇': if (direction != null) direction[0] = true; return '⦈';
+ case '⦈': if (direction != null) direction[0] = false; return '⦇';
+ case '⟦': if (direction != null) direction[0] = true; return '⟧';
+ case '⟧': if (direction != null) direction[0] = false; return '⟦';
+ case '⦃': if (direction != null) direction[0] = true; return '⦄';
+ case '⦄': if (direction != null) direction[0] = false; return '⦃';
default: return '\0';
}
} //}}}
diff -ru 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
--- 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2015-10-20 19:56:08.000000000 +0200
+++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-11-24 22:14:56.935661997 +0100
@@ -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,11 @@
Log.log(Log.ERROR,StandardUtilities.class,e);
}
}
-
- return styles;
+ styles[0] =
+ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
+ null, new Font(family, 0, size));
+ return _styleExtender.extendStyles(styles);
} //}}}
-
+
private SyntaxUtilities(){}
}