equal
deleted
inserted
replaced
1 --- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2018-04-09 01:58:01.000000000 +0200 |
|
2 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2019-07-17 21:36:43.985183582 +0200 |
|
3 @@ -1625,8 +1630,8 @@ |
|
4 } |
|
5 |
|
6 // Scan backwards, trying to find a bracket |
|
7 - String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃"; |
|
8 - String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄"; |
|
9 + String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"; |
|
10 + String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"; |
|
11 int count = 1; |
|
12 char openBracket = '\0'; |
|
13 char closeBracket = '\0'; |
|
14 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java |
|
15 --- 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2018-04-09 01:58:07.000000000 +0200 |
|
16 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2019-07-17 21:44:15.545431576 +0200 |
|
17 @@ -113,6 +113,8 @@ |
|
18 case '⟧': if (direction != null) direction[0] = false; return '⟦'; |
|
19 case '⦃': if (direction != null) direction[0] = true; return '⦄'; |
|
20 case '⦄': if (direction != null) direction[0] = false; return '⦃'; |
|
21 + case '⟪': if (direction != null) direction[0] = true; return '⟫'; |
|
22 + case '⟫': if (direction != null) direction[0] = false; return '⟪'; |
|
23 default: return '\0'; |
|
24 } |
|
25 } //}}} |
|