# HG changeset patch # User wenzelm # Date 1395756933 -3600 # Node ID c4f75e7338127f5d2b6d12403cc948a095e23698 # Parent 9e2d5e3debd3636888dc564746468fd088b8e449 separate "sml" mode, suppress old "ml" mode altogether; diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/lib/Tools/jedit --- 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,\n\n,; print qq,\n\n,; @@ -288,6 +287,10 @@ print qq,\n\n,; print; } + elsif (m/NAME="sqr"/) { + print qq!\n\n!; + print; + } else { print; } }' dist/modes/catalog diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/src/isabelle.scala --- 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. diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/src/modes/sml.xml --- /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 @@ + + + + + + + + + + + + + + + diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/src/token_markup.scala --- 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)))