separate "sml" mode, suppress old "ml" mode altogether;

--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 25 14:52:35 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 25 15:15:33 2014 +0100
@@ -61,6 +61,7 @@
   "src/modes/isabelle-options.xml"
   "src/modes/isabelle-root.xml"
   "src/modes/isabelle.xml"
+  "src/modes/sml.xml"
 )
 
 
@@ -277,9 +278,7 @@
   cp -p -R -f src/modes/. dist/modes/.
 
   perl -i -e 'while (<>) {
-    if (m/FILE_NAME_GLOB="\*\.{sml,ml}"/) {
-      print qq,\t\t\t\tFILE_NAME_GLOB="*.sml" />\n,;
-    }
+    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="\*\.{sml,ml}"/) { }
     elsif (m/NAME="javacc"/) {
       print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
       print qq,<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n,;
@@ -288,6 +287,10 @@
       print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,;
       print;
     }
+    elsif (m/NAME="sqr"/) {
+      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
+      print;
+    }
     else { print; }
   }' dist/modes/catalog
 

--- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 14:52:35 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 15:15:33 2014 +0100
@@ -29,7 +29,8 @@
       "isabelle-news",    // NEWS
       "isabelle-options", // etc/options
       "isabelle-output",  // pretty text area output
-      "isabelle-root")    // session ROOT
+      "isabelle-root",    // session ROOT
+      "sml")              // Standard ML (not Isabelle/ML)
 
   private lazy val ml_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/modes/sml.xml	Tue Mar 25 15:15:33 2014 +0100
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Standard ML mode -->
+<MODE>
+  <PROPS>
+    <PROPERTY NAME="commentStart" VALUE="(*"/>
+    <PROPERTY NAME="commentEnd" VALUE="*)"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'."/>
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
+    <PROPERTY NAME="tabSize" VALUE="2" />
+    <PROPERTY NAME="indentSize" VALUE="2" />
+  </PROPS>
+</MODE>

--- a/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 14:52:35 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 15:15:33 2014 +0100
@@ -203,7 +203,7 @@
       val context1 =
       {
         val (styled_tokens, context1) =
-          if (mode == "isabelle-ml") {
+          if (mode == "isabelle-ml" || mode == "sml") {
             val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
             val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
             (styled_tokens, new Line_Context(Some(ctxt1)))