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, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 70375 2e8af171887f
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70375
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     1
 
--- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-09 01:58:01.000000000 +0200
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     2
 
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2019-07-17 21:36:43.985183582 +0200
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     3
 
@@ -1625,8 +1630,8 @@
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     4
 
 		}
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     5
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     6
 
 		// Scan backwards, trying to find a bracket
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     7
 
-		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     8
 
-		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄";
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
     9
 
+		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    10
 
+		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    11
 
 		int count = 1;
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    12
 
 		char openBracket = '\0';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    13
 
 		char closeBracket = '\0';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    14
 
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    15
 
--- 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2018-04-09 01:58:07.000000000 +0200
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    16
 
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2019-07-17 21:44:15.545431576 +0200
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    17
 
@@ -113,6 +113,8 @@
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    18
 
 		case '⟧': if (direction != null) direction[0] = false; return '⟦';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    19
 
 		case '⦃': if (direction != null) direction[0] = true;  return '⦄';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    20
 
 		case '⦄': if (direction != null) direction[0] = false; return '⦃';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    21
 
+		case '⟪': if (direction != null) direction[0] = true;  return '⟫';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    22
 
+		case '⟫': if (direction != null) direction[0] = false; return '⟪';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    23
 
 		default:  return '\0';
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    24
 
 		}
2e8af171887f updated to jedit_build-20190717: support more brackets;
wenzelm
parents:
diff changeset 
    25
 
 	} //}}}
isabelle