src/Tools/jEdit/patches/brackets_extended_styles

proper syntax;

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(){}
 }