isabelle-ml mode with separate token marker;
clarified ML_Lex.gap_start: end-of-input counts as single newline;

--- a/src/Pure/ML/ml_lex.scala	Sat Feb 15 14:52:51 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:27:58 2014 +0100
@@ -32,6 +32,9 @@
   }
 
   sealed case class Token(val kind: Kind.Value, val source: String)
+  {
+    def is_operator: Boolean = kind == Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
+  }
 
 
 
@@ -52,10 +55,11 @@
   {
     /* string material */
 
+    private val blanks = many(character(Symbol.is_ascii_blank))
     private val blanks1 = many1(character(Symbol.is_ascii_blank))
 
     private val gap = "\\" ~ blanks1 ~ "\\" ^^ { case x ~ y ~ z => x + y + z }
-    private val gap_start = "\\" ~ blanks1 ~ """\z""".r ^^ { case x ~ y ~ _ => x + y }
+    private val gap_start = "\\" ~ blanks ~ """\z""".r ^^ { case x ~ y ~ _ => x + y }
 
     private val escape =
       one(character("\"\\abtnvfr".contains(_))) |
@@ -96,7 +100,7 @@
           "\"" ~ ml_string_body ~ ("\"" | gap_start) ^^
             { case x ~ y ~ z => result(x + y + z, if (z == "\"") Scan.Finished else ML_String) }
         case ML_String =>
-          blanks1 ~ opt_term("\\" ~ ml_string_body ~ ("\"" | gap_start)) ^^
+          blanks ~ opt_term("\\" ~ ml_string_body ~ ("\"" | gap_start)) ^^
             { case x ~ Some(y ~ z ~ w) =>
                 result(x + y + z + w, if (w == "\"") Scan.Finished else ML_String)
               case x ~ None => result(x, ML_String) }

--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Feb 15 14:52:51 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Feb 15 16:27:58 2014 +0100
@@ -55,6 +55,7 @@
   "src/Isabelle.props"
   "src/jEdit.props"
   "src/services.xml"
+  "src/modes/isabelle-ml.xml"
   "src/modes/isabelle-news.xml"
   "src/modes/isabelle-options.xml"
   "src/modes/isabelle-root.xml"
@@ -275,12 +276,19 @@
   cp -p -R -f src/modes/. dist/modes/.
 
   perl -i -e 'while (<>) {
-    if (m/NAME="javacc"/) {
+    if (m/FILE_NAME_GLOB="\*\.{sml,ml}"/) {
+      print qq,\t\t\t\tFILE_NAME_GLOB="*.sml" />\n,;
+    }
+    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,;
       print qq,<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n,;
       print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
-      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
-    print; }' dist/modes/catalog
+      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,;
+      print;
+    }
+    else { print; }
+  }' dist/modes/catalog
 
   cd dist
   isabelle_jdk jar xf jedit.jar

--- a/src/Tools/jEdit/src/isabelle.scala	Sat Feb 15 14:52:51 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Feb 15 16:27:58 2014 +0100
@@ -24,13 +24,14 @@
   val modes =
     List(
       "isabelle",         // theory source
+      "isabelle-ml",      // ML source
       "isabelle-markup",  // SideKick markup tree
       "isabelle-news",    // NEWS
       "isabelle-options", // etc/options
       "isabelle-output",  // pretty text area output
       "isabelle-root")    // session ROOT
 
-  private lazy val news_syntax = Outer_Syntax.init().no_tokens
+  private lazy val symbols_syntax = Outer_Syntax.init().no_tokens
 
   def mode_syntax(name: String): Option[Outer_Syntax] =
     name match {
@@ -39,7 +40,7 @@
         if (syntax == Outer_Syntax.empty) None else Some(syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Build.root_syntax)
-      case "isabelle-news" => Some(news_syntax)
+      case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax)
       case "isabelle-output" => None
       case _ => None
     }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/modes/isabelle-ml.xml	Sat Feb 15 16:27:58 2014 +0100
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Isabelle/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/rendering.scala	Sat Feb 15 14:52:51 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:27:58 2014 +0100
@@ -110,6 +110,29 @@
     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
     else if (token.is_operator) JEditToken.OPERATOR
     else token_style(token.kind)
+
+  private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
+  {
+    import JEditToken._
+    Map[ML_Lex.Kind.Value, Byte](
+      ML_Lex.Kind.KEYWORD -> KEYWORD1,
+      ML_Lex.Kind.IDENT -> NULL,
+      ML_Lex.Kind.LONG_IDENT -> NULL,
+      ML_Lex.Kind.TYPE_VAR -> NULL,
+      ML_Lex.Kind.WORD -> NULL,
+      ML_Lex.Kind.INT -> NULL,
+      ML_Lex.Kind.REAL -> NULL,
+      ML_Lex.Kind.CHAR -> LITERAL2,
+      ML_Lex.Kind.STRING -> LITERAL1,
+      ML_Lex.Kind.SPACE -> NULL,
+      ML_Lex.Kind.COMMENT -> COMMENT1,
+      ML_Lex.Kind.ERROR -> INVALID
+    ).withDefaultValue(NULL)
+  }
+
+  def ml_token_markup(token: ML_Lex.Token): Byte =
+    if (token.is_operator) JEditToken.OPERATOR
+    else ml_token_style(token.kind)
 }
 
 

--- a/src/Tools/jEdit/src/token_markup.scala	Sat Feb 15 14:52:51 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Feb 15 16:27:58 2014 +0100
@@ -203,21 +203,29 @@
       val context1 =
       {
         val (styled_tokens, context1) =
-          Isabelle.mode_syntax(mode) match {
-            case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
-              val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
-              val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok))
-              (styled_tokens, new Line_Context(Some(ctxt1)))
-            case _ =>
-              val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
-              (List((JEditToken.NULL, token)), new Line_Context(None))
+          if (mode == "isabelle-ml") {
+            val (tokens, ctxt1) = ML_Lex.tokenize_context(line, line_ctxt.get)
+            val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
+            (styled_tokens, new Line_Context(Some(ctxt1)))
+          }
+          else {
+            Isabelle.mode_syntax(mode) match {
+              case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
+                val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+                val styled_tokens =
+                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
+                (styled_tokens, new Line_Context(Some(ctxt1)))
+              case _ =>
+                val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+                (List(styled_token), new Line_Context(None))
+            }
           }
 
         val extended = extended_styles(line)
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
-          val length = token.source.length
+          val length = token.length
           val end_offset = offset + length
           if ((offset until end_offset) exists
               (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {