support more brackets (see also 427724cff970, 7bf637b65ba2);
authorwenzelm
Thu, 26 Sep 2013 16:30:32 +0200
changeset 55068239f8f451976
parent 55055 0fc622be0185
child 55069 f19be93909f1
support more brackets (see also 427724cff970, 7bf637b65ba2);
src/Tools/jEdit/patches/brackets
src/Tools/jEdit/src/modes/isabelle-news.xml
src/Tools/jEdit/src/modes/isabelle-options.xml
src/Tools/jEdit/src/modes/isabelle-root.xml
src/Tools/jEdit/src/modes/isabelle.xml
     1.1 --- a/src/Tools/jEdit/patches/brackets	Thu Sep 26 13:51:08 2013 +0200
     1.2 +++ b/src/Tools/jEdit/patches/brackets	Thu Sep 26 16:30:32 2013 +0200
     1.3 @@ -1,3 +1,17 @@
     1.4 +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
     1.5 +--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2013-07-28 19:03:32.000000000 +0200
     1.6 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2013-09-26 16:09:50.131780476 +0200
     1.7 +@@ -1610,8 +1615,8 @@
     1.8 + 		}
     1.9 + 
    1.10 + 		// Scan backwards, trying to find a bracket
    1.11 +-		String openBrackets = "([{";
    1.12 +-		String closeBrackets = ")]}";
    1.13 ++		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
    1.14 ++		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
    1.15 + 		int count = 1;
    1.16 + 		char openBracket = '\0';
    1.17 + 		char closeBracket = '\0';
    1.18  diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
    1.19  --- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2013-07-28 19:03:24.000000000 +0200
    1.20  +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2013-09-05 10:51:09.996193290 +0200
     2.1 --- a/src/Tools/jEdit/src/modes/isabelle-news.xml	Thu Sep 26 13:51:08 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/modes/isabelle-news.xml	Thu Sep 26 16:30:32 2013 +0200
     2.3 @@ -5,8 +5,8 @@
     2.4  <MODE>
     2.5    <PROPS>
     2.6      <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     2.7 -    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
     2.8 -    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
     2.9 +    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
    2.10 +    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
    2.11      <PROPERTY NAME="tabSize" VALUE="2" />
    2.12      <PROPERTY NAME="indentSize" VALUE="2" />
    2.13    </PROPS>
     3.1 --- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Sep 26 13:51:08 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Sep 26 16:30:32 2013 +0200
     3.3 @@ -5,8 +5,8 @@
     3.4  <MODE>
     3.5    <PROPS>
     3.6      <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     3.7 -    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
     3.8 -    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
     3.9 +    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
    3.10 +    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
    3.11      <PROPERTY NAME="tabSize" VALUE="2" />
    3.12      <PROPERTY NAME="indentSize" VALUE="2" />
    3.13    </PROPS>
     4.1 --- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Sep 26 13:51:08 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Sep 26 16:30:32 2013 +0200
     4.3 @@ -5,8 +5,8 @@
     4.4  <MODE>
     4.5    <PROPS>
     4.6      <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     4.7 -    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
     4.8 -    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
     4.9 +    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
    4.10 +    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
    4.11      <PROPERTY NAME="tabSize" VALUE="2" />
    4.12      <PROPERTY NAME="indentSize" VALUE="2" />
    4.13    </PROPS>
     5.1 --- a/src/Tools/jEdit/src/modes/isabelle.xml	Thu Sep 26 13:51:08 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/modes/isabelle.xml	Thu Sep 26 16:30:32 2013 +0200
     5.3 @@ -7,8 +7,8 @@
     5.4      <PROPERTY NAME="commentStart" VALUE="(*"/>
     5.5      <PROPERTY NAME="commentEnd" VALUE="*)"/>
     5.6      <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     5.7 -    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
     5.8 -    <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
     5.9 +    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
    5.10 +    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
    5.11      <PROPERTY NAME="tabSize" VALUE="2" />
    5.12      <PROPERTY NAME="indentSize" VALUE="2" />
    5.13    </PROPS>