# HG changeset patch
# User wenzelm
# Date 1620664278 -7200
# Node ID f6b453449cc6ec66d61bca32ffd8e5648d2cb773
# Parent  dceb5dde442f49143a41b3e52fdf643ff5fbcc05
more brackets;

diff -r dceb5dde442f -r f6b453449cc6 src/Tools/jEdit/patches/extended_styles
--- 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(){}
- }
diff -r dceb5dde442f -r f6b453449cc6 src/Tools/jEdit/patches/extended_styles_brackets
--- /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(){}
+ }