separate "sml" mode, suppress old "ml" mode altogether;
authorwenzelm
Tue Mar 25 15:15:33 2014 +0100 (2014-03-25)
changeset 56277c4f75e733812
parent 56276 9e2d5e3debd3
child 56278 2576d3a40ed6
separate "sml" mode, suppress old "ml" mode altogether;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/modes/sml.xml
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 25 14:52:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 25 15:15:33 2014 +0100
     1.3 @@ -61,6 +61,7 @@
     1.4    "src/modes/isabelle-options.xml"
     1.5    "src/modes/isabelle-root.xml"
     1.6    "src/modes/isabelle.xml"
     1.7 +  "src/modes/sml.xml"
     1.8  )
     1.9  
    1.10  
    1.11 @@ -277,9 +278,7 @@
    1.12    cp -p -R -f src/modes/. dist/modes/.
    1.13  
    1.14    perl -i -e 'while (<>) {
    1.15 -    if (m/FILE_NAME_GLOB="\*\.{sml,ml}"/) {
    1.16 -      print qq,\t\t\t\tFILE_NAME_GLOB="*.sml" />\n,;
    1.17 -    }
    1.18 +    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="\*\.{sml,ml}"/) { }
    1.19      elsif (m/NAME="javacc"/) {
    1.20        print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
    1.21        print qq,<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n,;
    1.22 @@ -288,6 +287,10 @@
    1.23        print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,;
    1.24        print;
    1.25      }
    1.26 +    elsif (m/NAME="sqr"/) {
    1.27 +      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
    1.28 +      print;
    1.29 +    }
    1.30      else { print; }
    1.31    }' dist/modes/catalog
    1.32  
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 14:52:35 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 15:15:33 2014 +0100
     2.3 @@ -29,7 +29,8 @@
     2.4        "isabelle-news",    // NEWS
     2.5        "isabelle-options", // etc/options
     2.6        "isabelle-output",  // pretty text area output
     2.7 -      "isabelle-root")    // session ROOT
     2.8 +      "isabelle-root",    // session ROOT
     2.9 +      "sml")              // Standard ML (not Isabelle/ML)
    2.10  
    2.11    private lazy val ml_syntax: Outer_Syntax =
    2.12      Outer_Syntax.init().no_tokens.
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/modes/sml.xml	Tue Mar 25 15:15:33 2014 +0100
     3.3 @@ -0,0 +1,15 @@
     3.4 +<?xml version="1.0" encoding="UTF-8"?>
     3.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
     3.6 +
     3.7 +<!-- Standard ML mode -->
     3.8 +<MODE>
     3.9 +  <PROPS>
    3.10 +    <PROPERTY NAME="commentStart" VALUE="(*"/>
    3.11 +    <PROPERTY NAME="commentEnd" VALUE="*)"/>
    3.12 +    <PROPERTY NAME="noWordSep" VALUE="_'."/>
    3.13 +    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
    3.14 +    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
    3.15 +    <PROPERTY NAME="tabSize" VALUE="2" />
    3.16 +    <PROPERTY NAME="indentSize" VALUE="2" />
    3.17 +  </PROPS>
    3.18 +</MODE>
     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 14:52:35 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 15:15:33 2014 +0100
     4.3 @@ -203,7 +203,7 @@
     4.4        val context1 =
     4.5        {
     4.6          val (styled_tokens, context1) =
     4.7 -          if (mode == "isabelle-ml") {
     4.8 +          if (mode == "isabelle-ml" || mode == "sml") {
     4.9              val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
    4.10              val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
    4.11              (styled_tokens, new Line_Context(Some(ctxt1)))