# HG changeset patch
# User wenzelm
# Date 1460055260 -7200
# Node ID 5024d0c48e029d00a51cf42d61ed66ba3e1a9b3c
# Parent  d7009a515733b0b8b1104443cdbf6272976b35f4
clarified word syntax: "." is separator or delimiter;

diff -r d7009a515733 -r 5024d0c48e02 src/Tools/jEdit/src/modes/isabelle-ml.xml
--- a/src/Tools/jEdit/src/modes/isabelle-ml.xml	Thu Apr 07 20:51:52 2016 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-ml.xml	Thu Apr 07 20:54:20 2016 +0200
@@ -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 d7009a515733 -r 5024d0c48e02 src/Tools/jEdit/src/modes/isabelle-news.xml
--- a/src/Tools/jEdit/src/modes/isabelle-news.xml	Thu Apr 07 20:51:52 2016 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-news.xml	Thu Apr 07 20:54:20 2016 +0200
@@ -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 d7009a515733 -r 5024d0c48e02 src/Tools/jEdit/src/modes/isabelle-options.xml
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Apr 07 20:51:52 2016 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Apr 07 20:54:20 2016 +0200
@@ -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 d7009a515733 -r 5024d0c48e02 src/Tools/jEdit/src/modes/isabelle-root.xml
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Apr 07 20:51:52 2016 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Apr 07 20:54:20 2016 +0200
@@ -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 d7009a515733 -r 5024d0c48e02 src/Tools/jEdit/src/modes/isabelle.xml
--- a/src/Tools/jEdit/src/modes/isabelle.xml	Thu Apr 07 20:51:52 2016 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle.xml	Thu Apr 07 20:54:20 2016 +0200
@@ -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 d7009a515733 -r 5024d0c48e02 src/Tools/jEdit/src/modes/sml.xml
--- a/src/Tools/jEdit/src/modes/sml.xml	Thu Apr 07 20:51:52 2016 +0200
+++ b/src/Tools/jEdit/src/modes/sml.xml	Thu Apr 07 20:54:20 2016 +0200
@@ -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" />