Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/brackets
author wenzelm
Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978 8f4a332500e4
parent 53931 239f8f451976
child 59571 1081f91c0662
permissions -rw-r--r--
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53931
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     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
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     2
 
--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2013-07-28 19:03:32.000000000 +0200
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     3
 
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2013-09-26 16:09:50.131780476 +0200
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     4
 
@@ -1610,8 +1615,8 @@
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     5
 
 		}
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     6
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     7
 
 		// Scan backwards, trying to find a bracket
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     8
 
-		String openBrackets = "([{";
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
     9
 
-		String closeBrackets = ")]}";
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
    10
 
+		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
    11
 
+		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
    12
 
 		int count = 1;
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
    13
 
 		char openBracket = '\0';
239f8f451976 support more brackets (see also 427724cff970, 7bf637b65ba2);
wenzelm
parents: 53898
diff changeset 
    14
 
 		char closeBracket = '\0';
53415
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 53181
diff changeset 
    15
 
diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 53181
diff changeset 
    16
 
--- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2013-07-28 19:03:24.000000000 +0200
9ebab8b7d73c updated to jedit_build-20130905 which is based on jedit-5.1.0;
wenzelm
parents: 53181
diff changeset 
    17
 
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2013-09-05 10:51:09.996193290 +0200
53181
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    18
 
@@ -97,6 +97,22 @@
53133
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    19
 
 		case '}': if (direction != null) direction[0] = false; return '{';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    20
 
 		case '<': if (direction != null) direction[0] = true;  return '>';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    21
 
 		case '>': if (direction != null) direction[0] = false; return '<';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    22
 
+		case '«': if (direction != null) direction[0] = true;  return '»';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    23
 
+		case '»': if (direction != null) direction[0] = false; return '«';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    24
 
+		case '‹': if (direction != null) direction[0] = true;  return '›';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    25
 
+		case '›': if (direction != null) direction[0] = false; return '‹';
53181
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    26
 
+		case '⟨': if (direction != null) direction[0] = true;  return '⟩';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    27
 
+		case '⟩': if (direction != null) direction[0] = false; return '⟨';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    28
 
+		case '⌈': if (direction != null) direction[0] = true;  return '⌉';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    29
 
+		case '⌉': if (direction != null) direction[0] = false; return '⌈';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    30
 
+		case '⌊': if (direction != null) direction[0] = true;  return '⌋';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    31
 
+		case '⌋': if (direction != null) direction[0] = false; return '⌊';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    32
 
+		case '⦇': if (direction != null) direction[0] = true;  return '⦈';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    33
 
+		case '⦈': if (direction != null) direction[0] = false; return '⦇';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    34
 
+		case '⟦': if (direction != null) direction[0] = true;  return '⟧';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    35
 
+		case '⟧': if (direction != null) direction[0] = false; return '⟦';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    36
 
+		case '⦃': if (direction != null) direction[0] = true;  return '⦄';
7bf637b65ba2 support more brackets;
wenzelm
parents: 53133
diff changeset 
    37
 
+		case '⦄': if (direction != null) direction[0] = false; return '⦃';
53133
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    38
 
 		default:  return '\0';
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    39
 
 		}
427724cff970 support more brackets;
wenzelm
parents:
diff changeset 
    40
 
 	} //}}}
isabelle