# HG changeset patch # User wenzelm # Date 1377117655 -7200 # Node ID 427724cff97082d7912b0483e06f13181658d92a # Parent 346acc4b05c091a86a1826bb31349b4d131f0541 support more brackets; more uniform isabelle modes; diff -r 346acc4b05c0 -r 427724cff970 src/Tools/jEdit/patches/jedit/brackets --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/jedit/brackets Wed Aug 21 22:40:55 2013 +0200 @@ -0,0 +1,15 @@ +diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java +--- 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2012-11-17 16:42:29.000000000 +0100 ++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-08-21 22:13:10.688736361 +0200 +@@ -97,6 +97,10 @@ + 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'; + } + } //}}} + diff -r 346acc4b05c0 -r 427724cff970 src/Tools/jEdit/src/modes/isabelle-news.xml --- a/src/Tools/jEdit/src/modes/isabelle-news.xml Wed Aug 21 21:41:44 2013 +0200 +++ b/src/Tools/jEdit/src/modes/isabelle-news.xml Wed Aug 21 22:40:55 2013 +0200 @@ -1,12 +1,12 @@ - + - - + + diff -r 346acc4b05c0 -r 427724cff970 src/Tools/jEdit/src/modes/isabelle-options.xml --- a/src/Tools/jEdit/src/modes/isabelle-options.xml Wed Aug 21 21:41:44 2013 +0200 +++ b/src/Tools/jEdit/src/modes/isabelle-options.xml Wed Aug 21 22:40:55 2013 +0200 @@ -1,12 +1,12 @@ - + - - + + diff -r 346acc4b05c0 -r 427724cff970 src/Tools/jEdit/src/modes/isabelle-root.xml --- a/src/Tools/jEdit/src/modes/isabelle-root.xml Wed Aug 21 21:41:44 2013 +0200 +++ b/src/Tools/jEdit/src/modes/isabelle-root.xml Wed Aug 21 22:40:55 2013 +0200 @@ -1,12 +1,12 @@ - + - - + + diff -r 346acc4b05c0 -r 427724cff970 src/Tools/jEdit/src/modes/isabelle.xml --- a/src/Tools/jEdit/src/modes/isabelle.xml Wed Aug 21 21:41:44 2013 +0200 +++ b/src/Tools/jEdit/src/modes/isabelle.xml Wed Aug 21 22:40:55 2013 +0200 @@ -1,4 +1,4 @@ - + @@ -7,8 +7,8 @@ - - + +