src/Tools/jEdit/patches/brackets

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/brackets	Wed Jul 17 21:56:32 2019 +0200
@@ -0,0 +1,25 @@
+--- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-09 01:58:01.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2019-07-17 21:36:43.985183582 +0200
+@@ -1625,8 +1630,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 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2018-04-09 01:58:07.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2019-07-17 21:44:15.545431576 +0200
+@@ -113,6 +113,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';
+ 		}
+ 	} //}}}