isabelle-ml mode with separate token marker;
authorwenzelm
Sat Feb 15 16:27:58 2014 +0100 (2014-02-15)
changeset 55500cdbbaa3074a8
parent 55499 2581fbee5b95
child 55501 fdde1d62e1fb
isabelle-ml mode with separate token marker;
clarified ML_Lex.gap_start: end-of-input counts as single newline;
src/Pure/ML/ml_lex.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/modes/isabelle-ml.xml
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/ML/ml_lex.scala	Sat Feb 15 14:52:51 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:27:58 2014 +0100
     1.3 @@ -32,6 +32,9 @@
     1.4    }
     1.5  
     1.6    sealed case class Token(val kind: Kind.Value, val source: String)
     1.7 +  {
     1.8 +    def is_operator: Boolean = kind == Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
     1.9 +  }
    1.10  
    1.11  
    1.12  
    1.13 @@ -52,10 +55,11 @@
    1.14    {
    1.15      /* string material */
    1.16  
    1.17 +    private val blanks = many(character(Symbol.is_ascii_blank))
    1.18      private val blanks1 = many1(character(Symbol.is_ascii_blank))
    1.19  
    1.20      private val gap = "\\" ~ blanks1 ~ "\\" ^^ { case x ~ y ~ z => x + y + z }
    1.21 -    private val gap_start = "\\" ~ blanks1 ~ """\z""".r ^^ { case x ~ y ~ _ => x + y }
    1.22 +    private val gap_start = "\\" ~ blanks ~ """\z""".r ^^ { case x ~ y ~ _ => x + y }
    1.23  
    1.24      private val escape =
    1.25        one(character("\"\\abtnvfr".contains(_))) |
    1.26 @@ -96,7 +100,7 @@
    1.27            "\"" ~ ml_string_body ~ ("\"" | gap_start) ^^
    1.28              { case x ~ y ~ z => result(x + y + z, if (z == "\"") Scan.Finished else ML_String) }
    1.29          case ML_String =>
    1.30 -          blanks1 ~ opt_term("\\" ~ ml_string_body ~ ("\"" | gap_start)) ^^
    1.31 +          blanks ~ opt_term("\\" ~ ml_string_body ~ ("\"" | gap_start)) ^^
    1.32              { case x ~ Some(y ~ z ~ w) =>
    1.33                  result(x + y + z + w, if (w == "\"") Scan.Finished else ML_String)
    1.34                case x ~ None => result(x, ML_String) }
     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Feb 15 14:52:51 2014 +0100
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Feb 15 16:27:58 2014 +0100
     2.3 @@ -55,6 +55,7 @@
     2.4    "src/Isabelle.props"
     2.5    "src/jEdit.props"
     2.6    "src/services.xml"
     2.7 +  "src/modes/isabelle-ml.xml"
     2.8    "src/modes/isabelle-news.xml"
     2.9    "src/modes/isabelle-options.xml"
    2.10    "src/modes/isabelle-root.xml"
    2.11 @@ -275,12 +276,19 @@
    2.12    cp -p -R -f src/modes/. dist/modes/.
    2.13  
    2.14    perl -i -e 'while (<>) {
    2.15 -    if (m/NAME="javacc"/) {
    2.16 +    if (m/FILE_NAME_GLOB="\*\.{sml,ml}"/) {
    2.17 +      print qq,\t\t\t\tFILE_NAME_GLOB="*.sml" />\n,;
    2.18 +    }
    2.19 +    elsif (m/NAME="javacc"/) {
    2.20        print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
    2.21 +      print qq,<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n,;
    2.22        print qq,<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n,;
    2.23        print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
    2.24 -      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
    2.25 -    print; }' dist/modes/catalog
    2.26 +      print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,;
    2.27 +      print;
    2.28 +    }
    2.29 +    else { print; }
    2.30 +  }' dist/modes/catalog
    2.31  
    2.32    cd dist
    2.33    isabelle_jdk jar xf jedit.jar
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Feb 15 14:52:51 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Feb 15 16:27:58 2014 +0100
     3.3 @@ -24,13 +24,14 @@
     3.4    val modes =
     3.5      List(
     3.6        "isabelle",         // theory source
     3.7 +      "isabelle-ml",      // ML source
     3.8        "isabelle-markup",  // SideKick markup tree
     3.9        "isabelle-news",    // NEWS
    3.10        "isabelle-options", // etc/options
    3.11        "isabelle-output",  // pretty text area output
    3.12        "isabelle-root")    // session ROOT
    3.13  
    3.14 -  private lazy val news_syntax = Outer_Syntax.init().no_tokens
    3.15 +  private lazy val symbols_syntax = Outer_Syntax.init().no_tokens
    3.16  
    3.17    def mode_syntax(name: String): Option[Outer_Syntax] =
    3.18      name match {
    3.19 @@ -39,7 +40,7 @@
    3.20          if (syntax == Outer_Syntax.empty) None else Some(syntax)
    3.21        case "isabelle-options" => Some(Options.options_syntax)
    3.22        case "isabelle-root" => Some(Build.root_syntax)
    3.23 -      case "isabelle-news" => Some(news_syntax)
    3.24 +      case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax)
    3.25        case "isabelle-output" => None
    3.26        case _ => None
    3.27      }
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/src/modes/isabelle-ml.xml	Sat Feb 15 16:27:58 2014 +0100
     4.3 @@ -0,0 +1,15 @@
     4.4 +<?xml version="1.0" encoding="UTF-8"?>
     4.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
     4.6 +
     4.7 +<!-- Isabelle/ML mode -->
     4.8 +<MODE>
     4.9 +  <PROPS>
    4.10 +    <PROPERTY NAME="commentStart" VALUE="(*"/>
    4.11 +    <PROPERTY NAME="commentEnd" VALUE="*)"/>
    4.12 +    <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
    4.13 +    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
    4.14 +    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
    4.15 +    <PROPERTY NAME="tabSize" VALUE="2" />
    4.16 +    <PROPERTY NAME="indentSize" VALUE="2" />
    4.17 +  </PROPS>
    4.18 +</MODE>
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 14:52:51 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:27:58 2014 +0100
     5.3 @@ -110,6 +110,29 @@
     5.4      if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
     5.5      else if (token.is_operator) JEditToken.OPERATOR
     5.6      else token_style(token.kind)
     5.7 +
     5.8 +  private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
     5.9 +  {
    5.10 +    import JEditToken._
    5.11 +    Map[ML_Lex.Kind.Value, Byte](
    5.12 +      ML_Lex.Kind.KEYWORD -> KEYWORD1,
    5.13 +      ML_Lex.Kind.IDENT -> NULL,
    5.14 +      ML_Lex.Kind.LONG_IDENT -> NULL,
    5.15 +      ML_Lex.Kind.TYPE_VAR -> NULL,
    5.16 +      ML_Lex.Kind.WORD -> NULL,
    5.17 +      ML_Lex.Kind.INT -> NULL,
    5.18 +      ML_Lex.Kind.REAL -> NULL,
    5.19 +      ML_Lex.Kind.CHAR -> LITERAL2,
    5.20 +      ML_Lex.Kind.STRING -> LITERAL1,
    5.21 +      ML_Lex.Kind.SPACE -> NULL,
    5.22 +      ML_Lex.Kind.COMMENT -> COMMENT1,
    5.23 +      ML_Lex.Kind.ERROR -> INVALID
    5.24 +    ).withDefaultValue(NULL)
    5.25 +  }
    5.26 +
    5.27 +  def ml_token_markup(token: ML_Lex.Token): Byte =
    5.28 +    if (token.is_operator) JEditToken.OPERATOR
    5.29 +    else ml_token_style(token.kind)
    5.30  }
    5.31  
    5.32  
     6.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Feb 15 14:52:51 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Feb 15 16:27:58 2014 +0100
     6.3 @@ -203,21 +203,29 @@
     6.4        val context1 =
     6.5        {
     6.6          val (styled_tokens, context1) =
     6.7 -          Isabelle.mode_syntax(mode) match {
     6.8 -            case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
     6.9 -              val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
    6.10 -              val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok))
    6.11 -              (styled_tokens, new Line_Context(Some(ctxt1)))
    6.12 -            case _ =>
    6.13 -              val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
    6.14 -              (List((JEditToken.NULL, token)), new Line_Context(None))
    6.15 +          if (mode == "isabelle-ml") {
    6.16 +            val (tokens, ctxt1) = ML_Lex.tokenize_context(line, line_ctxt.get)
    6.17 +            val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
    6.18 +            (styled_tokens, new Line_Context(Some(ctxt1)))
    6.19 +          }
    6.20 +          else {
    6.21 +            Isabelle.mode_syntax(mode) match {
    6.22 +              case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
    6.23 +                val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
    6.24 +                val styled_tokens =
    6.25 +                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
    6.26 +                (styled_tokens, new Line_Context(Some(ctxt1)))
    6.27 +              case _ =>
    6.28 +                val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    6.29 +                (List(styled_token), new Line_Context(None))
    6.30 +            }
    6.31            }
    6.32  
    6.33          val extended = extended_styles(line)
    6.34  
    6.35          var offset = 0
    6.36          for ((style, token) <- styled_tokens) {
    6.37 -          val length = token.source.length
    6.38 +          val length = token.length
    6.39            val end_offset = offset + length
    6.40            if ((offset until end_offset) exists
    6.41                (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {