--- a/src/Tools/jEdit/patches/extended_styles_brackets Fri Aug 22 22:45:30 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54.066016546 +0100
-@@ -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;
- //}}}
-
-@@ -926,6 +926,11 @@
- }
-
- @Override
-+ public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
-+ synchronized (this) { return super.computeIfAbsent(key, f); }
-+ }
-+
-+ @Override
- protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
- {
- return size() > capacity;
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-10-29 11:50:54.066016546 +0100
-@@ -919,6 +919,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.
-@@ -1627,8 +1632,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';
-@@ -4983,6 +4988,7 @@
- final Point offsetXY;
-
- boolean lastLinePartial;
-+ public boolean isLastLinePartial() { return lastLinePartial; }
-
- boolean blink;
- //}}}
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:54.066016546 +0100
-@@ -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';
- }
- } //}}}
--- a/src/Tools/jEdit/patches/main Fri Aug 22 22:45:30 2025 +0200
+++ b/src/Tools/jEdit/patches/main Sat Aug 23 12:35:32 2025 +0200
@@ -1,3 +1,87 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54.066016546 +0100
+@@ -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;
+ //}}}
+
+@@ -926,6 +926,11 @@
+ }
+
+ @Override
++ public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
++ synchronized (this) { return super.computeIfAbsent(key, f); }
++ }
++
++ @Override
+ protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
+ {
+ return size() > capacity;
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-10-29 11:50:54.066016546 +0100
+@@ -919,6 +919,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.
+@@ -1627,8 +1632,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';
+@@ -4983,6 +4988,7 @@
+ final Point offsetXY;
+
+ boolean lastLinePartial;
++ public boolean isLastLinePartial() { return lastLinePartial; }
+
+ boolean blink;
+ //}}}
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:54.066016546 +0100
+@@ -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.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-05-20 15:40:14.181962645 +0200