--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/brackets Wed Sep 25 20:29:28 2013 +0200
@@ -0,0 +1,26 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +0200
+@@ -97,6 +97,22 @@
+ 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 '«';
++ 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 '⟨';
++ 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 '⌊';
++ 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 '⟦';
++ case '⦃': if (direction != null) direction[0] = true; return '⦄';
++ case '⦄': if (direction != null) direction[0] = false; return '⦃';
+ default: return '\0';
+ }
+ } //}}}