53133
|
1 |
--- 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2012-11-17 16:42:29.000000000 +0100
|
53181
|
2 |
+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-08-24 15:58:43.075546141 +0200
|
|
3 |
@@ -97,6 +97,22 @@
|
53133
|
4 |
case '}': if (direction != null) direction[0] = false; return '{';
|
|
5 |
case '<': if (direction != null) direction[0] = true; return '>';
|
|
6 |
case '>': if (direction != null) direction[0] = false; return '<';
|
|
7 |
+ case '«': if (direction != null) direction[0] = true; return '»';
|
|
8 |
+ case '»': if (direction != null) direction[0] = false; return '«';
|
|
9 |
+ case '‹': if (direction != null) direction[0] = true; return '›';
|
|
10 |
+ case '›': if (direction != null) direction[0] = false; return '‹';
|
53181
|
11 |
+ case '⟨': if (direction != null) direction[0] = true; return '⟩';
|
|
12 |
+ case '⟩': if (direction != null) direction[0] = false; return '⟨';
|
|
13 |
+ case '⌈': if (direction != null) direction[0] = true; return '⌉';
|
|
14 |
+ case '⌉': if (direction != null) direction[0] = false; return '⌈';
|
|
15 |
+ case '⌊': if (direction != null) direction[0] = true; return '⌋';
|
|
16 |
+ case '⌋': if (direction != null) direction[0] = false; return '⌊';
|
|
17 |
+ case '⦇': if (direction != null) direction[0] = true; return '⦈';
|
|
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 '⦃';
|
53133
|
23 |
default: return '\0';
|
|
24 |
}
|
|
25 |
} //}}}
|