# HG changeset patch
# User wenzelm
# Date 1380206538 -7200
# Node ID f19be93909f11af1f2992aebee02633042002edd
# Parent  239f8f45197608719113f98f2828f9e27ab21412
more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);

diff -r 239f8f451976 -r f19be93909f1 src/Tools/jEdit/src/modes/isabelle-options.xml
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Sep 26 16:30:32 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Thu Sep 26 16:42:18 2013 +0200
@@ -4,6 +4,8 @@
 <!-- Isabelle options mode -->
 <MODE>
   <PROPS>
+    <PROPERTY NAME="commentStart" VALUE="(*"/>
+    <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
diff -r 239f8f451976 -r f19be93909f1 src/Tools/jEdit/src/modes/isabelle-root.xml
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Sep 26 16:30:32 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Thu Sep 26 16:42:18 2013 +0200
@@ -4,6 +4,8 @@
 <!-- Isabelle session root mode -->
 <MODE>
   <PROPS>
+    <PROPERTY NAME="commentStart" VALUE="(*"/>
+    <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
diff -r 239f8f451976 -r f19be93909f1 src/Tools/jEdit/src/modes/isabelle.xml
--- a/src/Tools/jEdit/src/modes/isabelle.xml	Thu Sep 26 16:30:32 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle.xml	Thu Sep 26 16:42:18 2013 +0200
@@ -12,22 +12,4 @@
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
-  <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
-    <SPAN TYPE="COMMENT1">
-      <BEGIN>(*</BEGIN>
-      <END>*)</END>
-    </SPAN>
-    <SPAN TYPE="COMMENT3">
-      <BEGIN>{*</BEGIN>
-      <END>*}</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL1">
-      <BEGIN>`</BEGIN>
-      <END>`</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL3">
-      <BEGIN>"</BEGIN>
-      <END>"</END>
-    </SPAN>
-  </RULES>
 </MODE>