separate tokenization and language context for SML: no symbols, no antiquotes;
authorwenzelm
Tue Mar 25 16:11:00 2014 +0100 (2014-03-25)
changeset 562782576d3a40ed6
parent 56277 c4f75e733812
child 56279 b4d874f6c6be
separate tokenization and language context for SML: no symbols, no antiquotes;
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/completion.scala
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/ML/ml_lex.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Mar 25 15:15:33 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Mar 25 16:11:00 2014 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4    | _ => error ("Single ML name expected in input: " ^ quote txt));
     1.5  
     1.6  fun prep_ml source =
     1.7 -  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source source);
     1.8 +  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
     1.9  
    1.10  fun index_ml name kind ml = Thy_Output.antiquotation name
    1.11    (Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position)))
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 15:15:33 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 16:11:00 2014 +0100
     2.3 @@ -118,7 +118,7 @@
     2.4        let
     2.5          val toks =
     2.6            ML_Lex.read Position.none "fn _ => (" @
     2.7 -          ML_Lex.read_source source @
     2.8 +          ML_Lex.read_source false source @
     2.9            ML_Lex.read Position.none ");";
    2.10          val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
    2.11        in "" end);
    2.12 @@ -189,7 +189,7 @@
    2.13        val ctxt' = ctxt |> Context.proof_map
    2.14          (ML_Context.expression (#pos source)
    2.15            "fun tactic (ctxt : Proof.context) : tactic"
    2.16 -          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source));
    2.17 +          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
    2.18      in Data.get ctxt' ctxt end;
    2.19  end;
    2.20  *}
     3.1 --- a/src/Pure/General/completion.scala	Tue Mar 25 15:15:33 2014 +0100
     3.2 +++ b/src/Pure/General/completion.scala	Tue Mar 25 16:11:00 2014 +0100
     3.3 @@ -193,6 +193,7 @@
     3.4      val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
     3.5      val ML_outer = Language_Context(Markup.Language.ML, false, true)
     3.6      val ML_inner = Language_Context(Markup.Language.ML, true, false)
     3.7 +    val SML_outer = Language_Context(Markup.Language.SML, false, false)
     3.8    }
     3.9  
    3.10    sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
     4.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 25 15:15:33 2014 +0100
     4.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 25 16:11:00 2014 +0100
     4.3 @@ -181,7 +181,7 @@
     4.4      "val (name, scan, comment): binding * attribute context_parser * string"
     4.5      "Context.map_theory (Attrib.setup name scan comment)"
     4.6      (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
     4.7 -      ML_Lex.read_source source @
     4.8 +      ML_Lex.read_source false source @
     4.9        ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    4.10  
    4.11  
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 15:15:33 2014 +0100
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 16:11:00 2014 +0100
     5.3 @@ -67,12 +67,12 @@
     5.4  (* generic setup *)
     5.5  
     5.6  fun global_setup source =
     5.7 -  ML_Lex.read_source source
     5.8 +  ML_Lex.read_source false source
     5.9    |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
    5.10    |> Context.theory_map;
    5.11  
    5.12  fun local_setup source =
    5.13 -  ML_Lex.read_source source
    5.14 +  ML_Lex.read_source false source
    5.15    |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
    5.16    |> Context.proof_map;
    5.17  
    5.18 @@ -80,35 +80,35 @@
    5.19  (* translation functions *)
    5.20  
    5.21  fun parse_ast_translation source =
    5.22 -  ML_Lex.read_source source
    5.23 +  ML_Lex.read_source false source
    5.24    |> ML_Context.expression (#pos source)
    5.25      "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    5.26      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    5.27    |> Context.theory_map;
    5.28  
    5.29  fun parse_translation source =
    5.30 -  ML_Lex.read_source source
    5.31 +  ML_Lex.read_source false source
    5.32    |> ML_Context.expression (#pos source)
    5.33      "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    5.34      "Context.map_theory (Sign.parse_translation parse_translation)"
    5.35    |> Context.theory_map;
    5.36  
    5.37  fun print_translation source =
    5.38 -  ML_Lex.read_source source
    5.39 +  ML_Lex.read_source false source
    5.40    |> ML_Context.expression (#pos source)
    5.41      "val print_translation: (string * (Proof.context -> term list -> term)) list"
    5.42      "Context.map_theory (Sign.print_translation print_translation)"
    5.43    |> Context.theory_map;
    5.44  
    5.45  fun typed_print_translation source =
    5.46 -  ML_Lex.read_source source
    5.47 +  ML_Lex.read_source false source
    5.48    |> ML_Context.expression (#pos source)
    5.49      "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    5.50      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    5.51    |> Context.theory_map;
    5.52  
    5.53  fun print_ast_translation source =
    5.54 -  ML_Lex.read_source source
    5.55 +  ML_Lex.read_source false source
    5.56    |> ML_Context.expression (#pos source)
    5.57      "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    5.58      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    5.59 @@ -135,7 +135,7 @@
    5.60  
    5.61  fun oracle (name, pos) source =
    5.62    let
    5.63 -    val body = ML_Lex.read_source source;
    5.64 +    val body = ML_Lex.read_source false source;
    5.65      val ants =
    5.66        ML_Lex.read Position.none
    5.67         ("local\n\
    5.68 @@ -162,7 +162,7 @@
    5.69  (* declarations *)
    5.70  
    5.71  fun declaration {syntax, pervasive} source =
    5.72 -  ML_Lex.read_source source
    5.73 +  ML_Lex.read_source false source
    5.74    |> ML_Context.expression (#pos source)
    5.75      "val declaration: Morphism.declaration"
    5.76      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    5.77 @@ -173,7 +173,7 @@
    5.78  (* simprocs *)
    5.79  
    5.80  fun simproc_setup name lhss source identifier =
    5.81 -  ML_Lex.read_source source
    5.82 +  ML_Lex.read_source false source
    5.83    |> ML_Context.expression (#pos source)
    5.84      "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
    5.85      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
     6.1 --- a/src/Pure/Isar/method.ML	Tue Mar 25 15:15:33 2014 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Tue Mar 25 16:11:00 2014 +0100
     6.3 @@ -269,7 +269,7 @@
     6.4      val ctxt' = ctxt |> Context.proof_map
     6.5        (ML_Context.expression (#pos source)
     6.6          "fun tactic (facts: thm list) : tactic"
     6.7 -        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source source));
     6.8 +        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source false source));
     6.9    in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
    6.10  
    6.11  fun tactic source ctxt = METHOD (ml_tactic source ctxt);
    6.12 @@ -368,7 +368,7 @@
    6.13      "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
    6.14      "Context.map_theory (Method.setup name scan comment)"
    6.15      (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    6.16 -      ML_Lex.read_source source @
    6.17 +      ML_Lex.read_source false source @
    6.18        ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    6.19  
    6.20  
     7.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 25 15:15:33 2014 +0100
     7.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 25 16:11:00 2014 +0100
     7.3 @@ -176,7 +176,7 @@
     7.4    in eval flags pos (ML_Lex.read pos (File.read path)) end;
     7.5  
     7.6  fun eval_source flags source =
     7.7 -  eval flags (#pos source) (ML_Lex.read_source source);
     7.8 +  eval flags (#pos source) (ML_Lex.read_source (#SML flags) source);
     7.9  
    7.10  fun eval_in ctxt flags pos ants =
    7.11    Context.setmp_thread_data (Option.map Context.Proof ctxt)
     8.1 --- a/src/Pure/ML/ml_lex.ML	Tue Mar 25 15:15:33 2014 +0100
     8.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Mar 25 16:11:00 2014 +0100
     8.3 @@ -26,7 +26,7 @@
     8.4        Source.source) Source.source
     8.5    val tokenize: string -> token list
     8.6    val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
     8.7 -  val read_source: Symbol_Pos.source -> token Antiquote.antiquote list
     8.8 +  val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list
     8.9  end;
    8.10  
    8.11  structure ML_Lex: ML_LEX =
    8.12 @@ -132,7 +132,7 @@
    8.13  
    8.14  local
    8.15  
    8.16 -val token_kind_markup =
    8.17 +fun token_kind_markup SML =
    8.18   fn Keyword   => (Markup.empty, "")
    8.19    | Ident     => (Markup.empty, "")
    8.20    | LongIdent => (Markup.empty, "")
    8.21 @@ -141,18 +141,18 @@
    8.22    | Int       => (Markup.ML_numeral, "")
    8.23    | Real      => (Markup.ML_numeral, "")
    8.24    | Char      => (Markup.ML_char, "")
    8.25 -  | String    => (Markup.ML_string, "")
    8.26 +  | String    => (if SML then Markup.SML_string else Markup.ML_string, "")
    8.27    | Space     => (Markup.empty, "")
    8.28 -  | Comment   => (Markup.ML_comment, "")
    8.29 +  | Comment   => (if SML then Markup.SML_comment else Markup.ML_comment, "")
    8.30    | Error msg => (Markup.bad, msg)
    8.31    | EOF       => (Markup.empty, "");
    8.32  
    8.33  in
    8.34  
    8.35 -fun report_of_token (tok as Token ((pos, _), (kind, x))) =
    8.36 +fun report_of_token SML (tok as Token ((pos, _), (kind, x))) =
    8.37    let
    8.38      val (markup, txt) =
    8.39 -      if not (is_keyword tok) then token_kind_markup kind
    8.40 +      if not (is_keyword tok) then token_kind_markup SML kind
    8.41        else if is_delimiter tok then (Markup.ML_delimiter, "")
    8.42        else if member (op =) keywords2 x then (Markup.ML_keyword2, "")
    8.43        else if member (op =) keywords3 x then (Markup.ML_keyword3, "")
    8.44 @@ -291,15 +291,7 @@
    8.45    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
    8.46    >> (single o token (Error msg));
    8.47  
    8.48 -in
    8.49 -
    8.50 -fun source src =
    8.51 -  Symbol_Pos.source (Position.line 1) src
    8.52 -  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
    8.53 -
    8.54 -val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
    8.55 -
    8.56 -fun read pos text =
    8.57 +fun gen_read SML pos text =
    8.58    let
    8.59      val syms = Symbol_Pos.explode (text, pos);
    8.60      val termination =
    8.61 @@ -309,17 +301,32 @@
    8.62            val pos1 = List.last syms |-> Position.advance;
    8.63            val pos2 = Position.advance Symbol.space pos1;
    8.64          in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
    8.65 +
    8.66 +    val scan = if SML then scan_ml >> Antiquote.Text else scan_antiq;
    8.67 +    fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
    8.68 +      | check _ = ();
    8.69      val input =
    8.70 -      (Source.of_list syms
    8.71 -        |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    8.72 -          (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    8.73 -        |> Source.exhaust
    8.74 -        |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token))
    8.75 -        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
    8.76 +      Source.of_list syms
    8.77 +      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan))
    8.78 +        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    8.79 +      |> Source.exhaust
    8.80 +      |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token SML))
    8.81 +      |> tap (List.app check);
    8.82    in input @ termination end;
    8.83  
    8.84 -fun read_source {delimited, text, pos} =
    8.85 -  (Position.report pos (Markup.language_ML delimited); read pos text);
    8.86 +in
    8.87 +
    8.88 +fun source src =
    8.89 +  Symbol_Pos.source (Position.line 1) src
    8.90 +  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
    8.91 +
    8.92 +val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
    8.93 +
    8.94 +val read = gen_read false;
    8.95 +
    8.96 +fun read_source SML {delimited, text, pos} =
    8.97 +  (Position.report pos ((if SML then Markup.language_SML else Markup.language_ML) delimited);
    8.98 +   gen_read SML pos text);
    8.99  
   8.100  end;
   8.101  
     9.1 --- a/src/Pure/ML/ml_lex.scala	Tue Mar 25 15:15:33 2014 +0100
     9.2 +++ b/src/Pure/ML/ml_lex.scala	Tue Mar 25 16:11:00 2014 +0100
     9.3 @@ -239,13 +239,15 @@
     9.4  
     9.5      def token: Parser[Token] = delimited_token | other_token
     9.6  
     9.7 -    def token_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
     9.8 +    def token_line(SML: Boolean, ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
     9.9      {
    9.10        val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished))
    9.11  
    9.12 -      ml_string_line(ctxt) |
    9.13 -        (ml_comment_line(ctxt) |
    9.14 -          (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
    9.15 +      if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
    9.16 +      else
    9.17 +        ml_string_line(ctxt) |
    9.18 +          (ml_comment_line(ctxt) |
    9.19 +            (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
    9.20      }
    9.21    }
    9.22  
    9.23 @@ -260,14 +262,14 @@
    9.24      }
    9.25    }
    9.26  
    9.27 -  def tokenize_line(input: CharSequence, context: Scan.Line_Context)
    9.28 +  def tokenize_line(SML: Boolean, input: CharSequence, context: Scan.Line_Context)
    9.29      : (List[Token], Scan.Line_Context) =
    9.30    {
    9.31      var in: Reader[Char] = new CharSequenceReader(input)
    9.32      val toks = new mutable.ListBuffer[Token]
    9.33      var ctxt = context
    9.34      while (!in.atEnd) {
    9.35 -      Parsers.parse(Parsers.token_line(ctxt), in) match {
    9.36 +      Parsers.parse(Parsers.token_line(SML, ctxt), in) match {
    9.37          case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    9.38          case Parsers.NoSuccess(_, rest) =>
    9.39            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    10.1 --- a/src/Pure/PIDE/markup.ML	Tue Mar 25 15:15:33 2014 +0100
    10.2 +++ b/src/Pure/PIDE/markup.ML	Tue Mar 25 16:11:00 2014 +0100
    10.3 @@ -33,6 +33,7 @@
    10.4    val language_term: bool -> T
    10.5    val language_prop: bool -> T
    10.6    val language_ML: bool -> T
    10.7 +  val language_SML: bool -> T
    10.8    val language_document: bool -> T
    10.9    val language_antiquotation: T
   10.10    val language_text: bool -> T
   10.11 @@ -93,6 +94,8 @@
   10.12    val ML_charN: string val ML_char: T
   10.13    val ML_stringN: string val ML_string: T
   10.14    val ML_commentN: string val ML_comment: T
   10.15 +  val SML_stringN: string val SML_string: T
   10.16 +  val SML_commentN: string val SML_comment: T
   10.17    val ML_defN: string
   10.18    val ML_openN: string
   10.19    val ML_structureN: string
   10.20 @@ -287,6 +290,7 @@
   10.21  val language_term = language' {name = "term", symbols = true, antiquotes = false};
   10.22  val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
   10.23  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
   10.24 +val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
   10.25  val language_document = language' {name = "document", symbols = false, antiquotes = true};
   10.26  val language_antiquotation =
   10.27    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
   10.28 @@ -398,6 +402,8 @@
   10.29  val (ML_charN, ML_char) = markup_elem "ML_char";
   10.30  val (ML_stringN, ML_string) = markup_elem "ML_string";
   10.31  val (ML_commentN, ML_comment) = markup_elem "ML_comment";
   10.32 +val (SML_stringN, SML_string) = markup_elem "SML_string";
   10.33 +val (SML_commentN, SML_comment) = markup_elem "SML_comment";
   10.34  
   10.35  val ML_defN = "ML_def";
   10.36  val ML_openN = "ML_open";
    11.1 --- a/src/Pure/PIDE/markup.scala	Tue Mar 25 15:15:33 2014 +0100
    11.2 +++ b/src/Pure/PIDE/markup.scala	Tue Mar 25 16:11:00 2014 +0100
    11.3 @@ -101,6 +101,7 @@
    11.4    object Language
    11.5    {
    11.6      val ML = "ML"
    11.7 +    val SML = "SML"
    11.8      val UNKNOWN = "unknown"
    11.9  
   11.10      def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
   11.11 @@ -202,6 +203,8 @@
   11.12    val ML_CHAR = "ML_char"
   11.13    val ML_STRING = "ML_string"
   11.14    val ML_COMMENT = "ML_comment"
   11.15 +  val SML_STRING = "SML_string"
   11.16 +  val SML_COMMENT = "SML_comment"
   11.17  
   11.18    val ML_DEF = "ML_def"
   11.19    val ML_OPEN = "ML_open"
    12.1 --- a/src/Pure/Thy/thy_output.ML	Tue Mar 25 15:15:33 2014 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 25 16:11:00 2014 +0100
    12.3 @@ -648,7 +648,7 @@
    12.4  
    12.5  fun ml_enclose bg en source =
    12.6    ML_Lex.read Position.none bg @
    12.7 -  ML_Lex.read_source source @
    12.8 +  ML_Lex.read_source false source @
    12.9    ML_Lex.read Position.none en;
   12.10  
   12.11  in
    13.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 15:15:33 2014 +0100
    13.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 16:11:00 2014 +0100
    13.3 @@ -36,6 +36,10 @@
    13.4      Outer_Syntax.init().no_tokens.
    13.5        set_language_context(Completion.Language_Context.ML_outer)
    13.6  
    13.7 +  private lazy val sml_syntax: Outer_Syntax =
    13.8 +    Outer_Syntax.init().no_tokens.
    13.9 +      set_language_context(Completion.Language_Context.SML_outer)
   13.10 +
   13.11    private lazy val news_syntax: Outer_Syntax =
   13.12      Outer_Syntax.init().no_tokens
   13.13  
   13.14 @@ -49,6 +53,7 @@
   13.15        case "isabelle-ml" => Some(ml_syntax)
   13.16        case "isabelle-news" => Some(news_syntax)
   13.17        case "isabelle-output" => None
   13.18 +      case "sml" => Some(sml_syntax)
   13.19        case _ => None
   13.20      }
   13.21  
    14.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Mar 25 15:15:33 2014 +0100
    14.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Mar 25 16:11:00 2014 +0100
    14.3 @@ -681,7 +681,9 @@
    14.4        Markup.ML_NUMERAL -> inner_numeral_color,
    14.5        Markup.ML_CHAR -> inner_quoted_color,
    14.6        Markup.ML_STRING -> inner_quoted_color,
    14.7 -      Markup.ML_COMMENT -> inner_comment_color)
    14.8 +      Markup.ML_COMMENT -> inner_comment_color,
    14.9 +      Markup.SML_STRING -> inner_quoted_color,
   14.10 +      Markup.SML_COMMENT -> inner_comment_color)
   14.11  
   14.12    private lazy val text_color_elements =
   14.13      Document.Elements(text_colors.keySet)
    15.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 15:15:33 2014 +0100
    15.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 16:11:00 2014 +0100
    15.3 @@ -204,7 +204,7 @@
    15.4        {
    15.5          val (styled_tokens, context1) =
    15.6            if (mode == "isabelle-ml" || mode == "sml") {
    15.7 -            val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
    15.8 +            val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get)
    15.9              val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
   15.10              (styled_tokens, new Line_Context(Some(ctxt1)))
   15.11            }