--- 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';
- }
- } //}}}