# HG changeset patch
# User wenzelm
# Date 1380205832 -7200
# Node ID 239f8f45197608719113f98f2828f9e27ab21412
# Parent  0fc622be018571a1859437396d10d66ad839a671
support more brackets (see also 427724cff970, 7bf637b65ba2);

diff -r 0fc622be0185 -r 239f8f451976 src/Tools/jEdit/patches/brackets
--- a/src/Tools/jEdit/patches/brackets	Thu Sep 26 13:51:08 2013 +0200
+++ b/src/Tools/jEdit/patches/brackets	Thu Sep 26 16:30:32 2013 +0200
@@ -1,3 +1,17 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2013-07-28 19:03:32.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2013-09-26 16:09:50.131780476 +0200
+@@ -1610,8 +1615,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.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
diff -r 0fc622be0185 -r 239f8f451976 src/Tools/jEdit/src/modes/isabelle-news.xml
--- a/src/Tools/jEdit/src/modes/isabelle-news.xml	Thu Sep 26 13:51:08 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-news.xml	Thu Sep 26 16:30:32 2013 +0200
@@ -5,8 +5,8 @@
 <MODE>
   <PROPS>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
diff -r 0fc622be0185 -r 239f8f451976 src/Tools/jEdit/src/modes/isabelle-options.xml
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Sep 26 13:51:08 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Sep 26 16:30:32 2013 +0200
@@ -5,8 +5,8 @@
 <MODE>
   <PROPS>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
diff -r 0fc622be0185 -r 239f8f451976 src/Tools/jEdit/src/modes/isabelle-root.xml
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Sep 26 13:51:08 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Sep 26 16:30:32 2013 +0200
@@ -5,8 +5,8 @@
 <MODE>
   <PROPS>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
diff -r 0fc622be0185 -r 239f8f451976 src/Tools/jEdit/src/modes/isabelle.xml
--- a/src/Tools/jEdit/src/modes/isabelle.xml	Thu Sep 26 13:51:08 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle.xml	Thu Sep 26 16:30:32 2013 +0200
@@ -7,8 +7,8 @@
     <PROPERTY NAME="commentStart" VALUE="(*"/>
     <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>