Mercurial Mercurial > repos > isabelle / file revision
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
Wed, 25 Sep 2013 20:29:28 +0200
changeset 53898 e4825d4c6bd7
parent 53415 src/Tools/jEdit/patches/jedit/brackets@9ebab8b7d73c
child 53931 239f8f451976
permissions -rw-r--r--
simplified directory structure;

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
@@ -97,6 +97,22 @@
 		case '}': if (direction != null) direction[0] = false; return '{';
 		case '<': if (direction != null) direction[0] = true;  return '>';
 		case '>': if (direction != null) direction[0] = false; return '<';
+		case '«': if (direction != null) direction[0] = true;  return '»';
+		case '»': if (direction != null) direction[0] = false; return '«';
+		case '‹': if (direction != null) direction[0] = true;  return '›';
+		case '›': if (direction != null) direction[0] = false; return '‹';
+		case '⟨': if (direction != null) direction[0] = true;  return '⟩';
+		case '⟩': if (direction != null) direction[0] = false; return '⟨';
+		case '⌈': if (direction != null) direction[0] = true;  return '⌉';
+		case '⌉': if (direction != null) direction[0] = false; return '⌈';
+		case '⌊': if (direction != null) direction[0] = true;  return '⌋';
+		case '⌋': if (direction != null) direction[0] = false; return '⌊';
+		case '⦇': if (direction != null) direction[0] = true;  return '⦈';
+		case '⦈': if (direction != null) direction[0] = false; return '⦇';
+		case '⟦': if (direction != null) direction[0] = true;  return '⟧';
+		case '⟧': if (direction != null) direction[0] = false; return '⟦';
+		case '⦃': if (direction != null) direction[0] = true;  return '⦄';
+		case '⦄': if (direction != null) direction[0] = false; return '⦃';
 		default:  return '\0';
 		}
 	} //}}}
isabelle