# HG changeset patch
# User wenzelm
# Date 1377353175 -7200
# Node ID 7bf637b65ba27c0fe05cba5d83288bae570b1251
# Parent  04590977dc3cb9eece3bd15901a0f94b30a9da35
support more brackets;

diff -r 04590977dc3c -r 7bf637b65ba2 src/Tools/jEdit/patches/jedit/brackets
--- a/src/Tools/jEdit/patches/jedit/brackets	Sat Aug 24 15:34:09 2013 +0200
+++ b/src/Tools/jEdit/patches/jedit/brackets	Sat Aug 24 16:06:15 2013 +0200
@@ -1,7 +1,6 @@
-diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
 --- 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2013-08-21 22:13:10.688736361 +0200
-@@ -97,6 +97,10 @@
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2013-08-24 15:58:43.075546141 +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 '<';
@@ -9,7 +8,18 @@
 +		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';
  		}
  	} //}}}
-