src/Tools/jEdit/patches/brackets
changeset 53931 239f8f451976
parent 53898 e4825d4c6bd7
child 59571 1081f91c0662
equal deleted inserted replaced
53918:0fc622be0185 53931:239f8f451976
       
     1 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
       
     2 --- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2013-07-28 19:03:32.000000000 +0200
       
     3 +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2013-09-26 16:09:50.131780476 +0200
       
     4 @@ -1610,8 +1615,8 @@
       
     5  		}
       
     6  
       
     7  		// Scan backwards, trying to find a bracket
       
     8 -		String openBrackets = "([{";
       
     9 -		String closeBrackets = ")]}";
       
    10 +		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
       
    11 +		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
       
    12  		int count = 1;
       
    13  		char openBracket = '\0';
       
    14  		char closeBracket = '\0';
     1 diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
    15 diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
     2 --- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2013-07-28 19:03:24.000000000 +0200
    16 --- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2013-07-28 19:03:24.000000000 +0200
     3 +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2013-09-05 10:51:09.996193290 +0200
    17 +++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2013-09-05 10:51:09.996193290 +0200
     4 @@ -97,6 +97,22 @@
    18 @@ -97,6 +97,22 @@
     5  		case '}': if (direction != null) direction[0] = false; return '{';
    19  		case '}': if (direction != null) direction[0] = false; return '{';