src/Tools/jEdit/patches/extended_styles_brackets

treat map_filter similar to list_all, list_ex, list_ex1

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