more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);
authorwenzelm
Thu, 26 Sep 2013 16:42:18 +0200
changeset 53932 f19be93909f1
parent 53931 239f8f451976
child 53933 7924d61b50cf
more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);
src/Tools/jEdit/src/modes/isabelle-options.xml
src/Tools/jEdit/src/modes/isabelle-root.xml
src/Tools/jEdit/src/modes/isabelle.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="⦄⟧⦈⌋⌉⟩›»)]}" />
--- 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="⦄⟧⦈⌋⌉⟩›»)]}" />
--- 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>