# HG changeset patch
# User wenzelm
# Date 1458589119 -3600
# Node ID 0c9b1857504be72fdbd561450ff5e4ede2dc51d1
# Parent  45b8dd2d3827a8ec81cba19fb6b8ccdb7ac18a15
accomodate Isabelle identifiers with subscripts;

diff -r 45b8dd2d3827 -r 0c9b1857504b src/Tools/jEdit/src/modes/isabelle-ml.xml
--- a/src/Tools/jEdit/src/modes/isabelle-ml.xml	Mon Mar 21 20:22:07 2016 +0100
+++ b/src/Tools/jEdit/src/modes/isabelle-ml.xml	Mon Mar 21 20:38:39 2016 +0100
@@ -6,7 +6,7 @@
   <PROPS>
     <PROPERTY NAME="commentStart" VALUE="(*"/>
     <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'.?⇩"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
diff -r 45b8dd2d3827 -r 0c9b1857504b src/Tools/jEdit/src/modes/isabelle-news.xml
--- a/src/Tools/jEdit/src/modes/isabelle-news.xml	Mon Mar 21 20:22:07 2016 +0100
+++ b/src/Tools/jEdit/src/modes/isabelle-news.xml	Mon Mar 21 20:38:39 2016 +0100
@@ -4,7 +4,7 @@
 <!-- Isabelle NEWS mode -->
 <MODE>
   <PROPS>
-    <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'.?⇩"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
diff -r 45b8dd2d3827 -r 0c9b1857504b src/Tools/jEdit/src/modes/isabelle-options.xml
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Mon Mar 21 20:22:07 2016 +0100
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Mon Mar 21 20:38:39 2016 +0100
@@ -6,7 +6,7 @@
   <PROPS>
     <PROPERTY NAME="commentStart" VALUE="(*"/>
     <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'.?⇩"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
diff -r 45b8dd2d3827 -r 0c9b1857504b src/Tools/jEdit/src/modes/isabelle-root.xml
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Mon Mar 21 20:22:07 2016 +0100
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Mon Mar 21 20:38:39 2016 +0100
@@ -6,7 +6,7 @@
   <PROPS>
     <PROPERTY NAME="commentStart" VALUE="(*"/>
     <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'.?⇩"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
diff -r 45b8dd2d3827 -r 0c9b1857504b src/Tools/jEdit/src/modes/isabelle.xml
--- a/src/Tools/jEdit/src/modes/isabelle.xml	Mon Mar 21 20:22:07 2016 +0100
+++ b/src/Tools/jEdit/src/modes/isabelle.xml	Mon Mar 21 20:38:39 2016 +0100
@@ -6,7 +6,7 @@
   <PROPS>
     <PROPERTY NAME="commentStart" VALUE="(*"/>
     <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'.?⇩"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />