--- a/src/Tools/jEdit/patches/extended_styles Mon May 10 17:15:37 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +0200
-@@ -332,9 +332,9 @@
- //{{{ Package private members
-
- //{{{ Instance variables
-- SyntaxStyle style;
-+ public SyntaxStyle style;
- // set up after init()
-- float width;
-+ public float width;
- //}}}
-
- //{{{ Chunk constructor
-@@ -584,8 +584,8 @@
- // this is either style.getBackgroundColor() or
- // styles[defaultID].getBackgroundColor()
- private Color background;
-- private char[] chars;
-- private String str;
-+ public char[] chars;
-+ public String str;
- private GlyphData glyphData;
- //}}}
-
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2021-05-10 11:02:05.820257742 +0200
-@@ -914,6 +914,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.
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200
-@@ -344,8 +344,28 @@
- }
- }
-
-- 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);
- } //}}}
-
-+ /**
-+ * 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;
-+ }
-+
- private SyntaxUtilities(){}
- }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/extended_styles_brackets Mon May 10 18:31:18 2021 +0200
@@ -0,0 +1,97 @@
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +0200
+@@ -332,9 +332,9 @@
+ //{{{ Package private members
+
+ //{{{ Instance variables
+- SyntaxStyle style;
++ public SyntaxStyle style;
+ // set up after init()
+- float width;
++ public float width;
+ //}}}
+
+ //{{{ Chunk constructor
+@@ -584,8 +584,8 @@
+ // this is either style.getBackgroundColor() or
+ // styles[defaultID].getBackgroundColor()
+ private Color background;
+- private char[] chars;
+- private String str;
++ public char[] chars;
++ public String str;
+ private GlyphData glyphData;
+ //}}}
+
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2021-05-10 18:19:56.275495525 +0200
+@@ -914,6 +914,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.
+@@ -1622,8 +1627,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 jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2020-09-03 05:31:03.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2021-05-10 18:20:57.418571547 +0200
+@@ -115,6 +115,8 @@
+ 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 jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
+--- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200
+@@ -344,8 +344,28 @@
+ }
+ }
+
+- 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);
+ } //}}}
+
++ /**
++ * 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;
++ }
++
+ private SyntaxUtilities(){}
+ }