expand ML cartouches to Input.source;
authorwenzelm
Mon Dec 08 22:42:12 2014 +0100 (2014-12-08)
changeset 59112e670969f34df
parent 59111 c85e018be3a3
child 59113 3cded6b57a82
expand ML cartouches to Input.source;
tuned signature;
NEWS
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/antiquote.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/ML/ml_lex.scala
src/Pure/ML/ml_thms.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/NEWS	Mon Dec 08 16:04:50 2014 +0100
     1.2 +++ b/NEWS	Mon Dec 08 22:42:12 2014 +0100
     1.3 @@ -218,6 +218,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Cartouches within ML sources are turned into values of type
     1.8 +Input.source (with formal position information).
     1.9 +
    1.10  * Proper context for various elementary tactics: assume_tac,
    1.11  match_tac, compose_tac, Splitter.split_tac etc.  Minor
    1.12  INCOMPATIBILITY.
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Mon Dec 08 16:04:50 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Dec 08 22:42:12 2014 +0100
     2.3 @@ -260,4 +260,15 @@
     2.4  lemma "A \<and> B \<longrightarrow> B \<and> A"
     2.5    by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
     2.6  
     2.7 +
     2.8 +subsection \<open>ML syntax: input source\<close>
     2.9 +
    2.10 +ML \<open>
    2.11 +  val s: Input.source = \<open>abc\<close>;
    2.12 +  writeln ("Look here!" ^ Position.here (Input.pos_of s));
    2.13 +
    2.14 +  \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
    2.15 +    if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
    2.16 +\<close>
    2.17 +
    2.18  end
     3.1 --- a/src/Pure/General/antiquote.ML	Mon Dec 08 16:04:50 2014 +0100
     3.2 +++ b/src/Pure/General/antiquote.ML	Mon Dec 08 22:42:12 2014 +0100
     3.3 @@ -8,7 +8,6 @@
     3.4  sig
     3.5    type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
     3.6    datatype 'a antiquote = Text of 'a | Antiq of antiq
     3.7 -  val is_text: 'a antiquote -> bool
     3.8    val antiq_reports: antiq -> Position.report list
     3.9    val antiquote_reports: ('a -> Position.report_text list) ->
    3.10      'a antiquote list -> Position.report_text list
    3.11 @@ -25,9 +24,6 @@
    3.12  type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
    3.13  datatype 'a antiquote = Text of 'a | Antiq of antiq;
    3.14  
    3.15 -fun is_text (Text _) = true
    3.16 -  | is_text _ = false;
    3.17 -
    3.18  
    3.19  (* reports *)
    3.20  
     4.1 --- a/src/Pure/General/symbol_pos.ML	Mon Dec 08 16:04:50 2014 +0100
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Dec 08 22:42:12 2014 +0100
     4.3 @@ -37,7 +37,7 @@
     4.4      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
     4.5    type text = string
     4.6    val implode: T list -> text
     4.7 -  val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     4.8 +  val implode_range: Position.range -> T list -> text * Position.range
     4.9    val explode: text * Position.T -> T list
    4.10    val scan_ident: T list -> T list * T list
    4.11    val is_identifier: string -> bool
    4.12 @@ -238,7 +238,7 @@
    4.13  
    4.14  val implode = implode o pad;
    4.15  
    4.16 -fun implode_range pos1 pos2 syms =
    4.17 +fun implode_range (pos1, pos2) syms =
    4.18    let val syms' = (("", pos1) :: syms @ [("", pos2)])
    4.19    in (implode syms', range syms') end;
    4.20  
     5.1 --- a/src/Pure/Isar/token.ML	Mon Dec 08 16:04:50 2014 +0100
     5.2 +++ b/src/Pure/Isar/token.ML	Mon Dec 08 22:42:12 2014 +0100
     5.3 @@ -542,7 +542,7 @@
     5.4    Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
     5.5  
     5.6  fun token_range k (pos1, (ss, pos2)) =
     5.7 -  Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
     5.8 +  Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot);
     5.9  
    5.10  fun scan_token keywords = !!! "bad input"
    5.11    (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     6.1 --- a/src/Pure/ML/ml_antiquotation.ML	Mon Dec 08 16:04:50 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Mon Dec 08 22:42:12 2014 +0100
     6.3 @@ -6,7 +6,6 @@
     6.4  
     6.5  signature ML_ANTIQUOTATION =
     6.6  sig
     6.7 -  val variant: string -> Proof.context -> string * Proof.context
     6.8    val declaration: binding -> 'a context_parser ->
     6.9      (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
    6.10      theory -> theory
    6.11 @@ -17,24 +16,6 @@
    6.12  structure ML_Antiquotation: ML_ANTIQUOTATION =
    6.13  struct
    6.14  
    6.15 -(* unique names *)
    6.16 -
    6.17 -val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
    6.18 -
    6.19 -structure Names = Proof_Data
    6.20 -(
    6.21 -  type T = Name.context;
    6.22 -  fun init _ = init_context;
    6.23 -);
    6.24 -
    6.25 -fun variant a ctxt =
    6.26 -  let
    6.27 -    val names = Names.get ctxt;
    6.28 -    val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
    6.29 -    val ctxt' = Names.put names' ctxt;
    6.30 -  in (b, ctxt') end;
    6.31 -
    6.32 -
    6.33  (* define antiquotations *)
    6.34  
    6.35  fun declaration name scan body =
    6.36 @@ -47,25 +28,15 @@
    6.37    declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
    6.38  
    6.39  fun value name scan =
    6.40 -  declaration name scan (fn _ => fn s => fn ctxt =>
    6.41 -    let
    6.42 -      val (a, ctxt') = variant (Binding.name_of name) ctxt;
    6.43 -      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    6.44 -      val body = "Isabelle." ^ a;
    6.45 -    in (K (env, body), ctxt') end);
    6.46 +  declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
    6.47  
    6.48  
    6.49  (* basic antiquotations *)
    6.50  
    6.51  val _ = Theory.setup
    6.52   (declaration (Binding.make ("here", @{here})) (Scan.succeed ())
    6.53 -    (fn src => fn () => fn ctxt =>
    6.54 -      let
    6.55 -        val (a, ctxt') = variant "position" ctxt;
    6.56 -        val (_, pos) = Token.name_of_src src;
    6.57 -        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
    6.58 -        val body = "Isabelle." ^ a;
    6.59 -      in (K (env, body), ctxt') end) #>
    6.60 +    (fn src => fn () =>
    6.61 +      ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
    6.62  
    6.63    value (Binding.make ("binding", @{here}))
    6.64      (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
     7.1 --- a/src/Pure/ML/ml_antiquotations.ML	Mon Dec 08 16:04:50 2014 +0100
     7.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Mon Dec 08 22:42:12 2014 +0100
     7.3 @@ -20,7 +20,7 @@
     7.4        (fn src => fn output => fn ctxt =>
     7.5          let
     7.6            val (_, pos) = Token.name_of_src src;
     7.7 -          val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
     7.8 +          val (a, ctxt') = ML_Context.variant "output" ctxt;
     7.9            val env =
    7.10              "val " ^ a ^ ": string -> unit =\n\
    7.11              \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
    7.12 @@ -30,16 +30,6 @@
    7.13          in (K (env, body), ctxt') end));
    7.14  
    7.15  
    7.16 -(* embedded source *)
    7.17 -
    7.18 -val _ = Theory.setup
    7.19 - (ML_Antiquotation.value @{binding source}
    7.20 -    (Scan.lift Args.text_source_position >> (fn source =>
    7.21 -      "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^
    7.22 -        ML_Syntax.print_string (Input.text_of source) ^ " " ^
    7.23 -        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
    7.24 -
    7.25 -
    7.26  (* formal entities *)
    7.27  
    7.28  val _ = Theory.setup
     8.1 --- a/src/Pure/ML/ml_context.ML	Mon Dec 08 16:04:50 2014 +0100
     8.2 +++ b/src/Pure/ML/ml_context.ML	Mon Dec 08 22:42:12 2014 +0100
     8.3 @@ -13,7 +13,9 @@
     8.4    val thms: xstring -> thm list
     8.5    val exec: (unit -> unit) -> Context.generic -> Context.generic
     8.6    val check_antiquotation: Proof.context -> xstring * Position.T -> string
     8.7 +  val variant: string -> Proof.context -> string * Proof.context
     8.8    type decl = Proof.context -> string * string
     8.9 +  val value_decl: string -> string -> Proof.context -> decl * Proof.context
    8.10    val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
    8.11      theory -> theory
    8.12    val print_antiquotations: Proof.context -> unit
    8.13 @@ -50,9 +52,38 @@
    8.14  
    8.15  (** ML antiquotations **)
    8.16  
    8.17 +(* unique names *)
    8.18 +
    8.19 +structure Names = Proof_Data
    8.20 +(
    8.21 +  type T = Name.context;
    8.22 +  val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
    8.23 +  fun init _ = init_names;
    8.24 +);
    8.25 +
    8.26 +fun variant a ctxt =
    8.27 +  let
    8.28 +    val names = Names.get ctxt;
    8.29 +    val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
    8.30 +    val ctxt' = Names.put names' ctxt;
    8.31 +  in (b, ctxt') end;
    8.32 +
    8.33 +
    8.34 +(* decl *)
    8.35 +
    8.36 +type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
    8.37 +
    8.38 +fun value_decl a s ctxt =
    8.39 +  let
    8.40 +    val (b, ctxt') = variant a ctxt;
    8.41 +    val env = "val " ^ b ^ " = " ^ s ^ ";\n";
    8.42 +    val body = "Isabelle." ^ b;
    8.43 +    fun decl (_: Proof.context) = (env, body);
    8.44 +  in (decl, ctxt') end;
    8.45 +
    8.46 +
    8.47  (* theory data *)
    8.48  
    8.49 -type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
    8.50  structure Antiquotations = Theory_Data
    8.51  (
    8.52    type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
    8.53 @@ -101,6 +132,9 @@
    8.54  val end_env = ML_Lex.tokenize "end;";
    8.55  val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
    8.56  
    8.57 +fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok
    8.58 +  | expanding (Antiquote.Antiq _) = true;
    8.59 +
    8.60  in
    8.61  
    8.62  fun eval_antiquotes (ants, pos) opt_context =
    8.63 @@ -112,20 +146,32 @@
    8.64      val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
    8.65  
    8.66      val ((ml_env, ml_body), opt_ctxt') =
    8.67 -      if forall Antiquote.is_text ants
    8.68 +      if forall (not o expanding) ants
    8.69        then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
    8.70        else
    8.71          let
    8.72 -          fun no_decl _ = ([], []);
    8.73 +          fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    8.74  
    8.75 -          fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
    8.76 -            | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
    8.77 +          fun expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
    8.78                  let
    8.79                    val keywords = Thy_Header.get_keywords' ctxt;
    8.80                    val (decl, ctxt') =
    8.81                      apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
    8.82 -                  val decl' = decl #> apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    8.83 -                in (decl', ctxt') end;
    8.84 +                in (decl #> tokenize range, ctxt') end
    8.85 +            | expand (Antiquote.Text tok) ctxt =
    8.86 +                if ML_Lex.is_cartouche tok then
    8.87 +                  let
    8.88 +                    val range = ML_Lex.range_of tok;
    8.89 +                    val text =
    8.90 +                      Symbol_Pos.explode (ML_Lex.content_of tok, #1 range)
    8.91 +                      |> Symbol_Pos.cartouche_content
    8.92 +                      |> Symbol_Pos.implode_range range |> #1;
    8.93 +                    val (decl, ctxt') =
    8.94 +                      value_decl "input"
    8.95 +                        ("Input.source true " ^ ML_Syntax.print_string text  ^ " " ^
    8.96 +                          ML_Syntax.atomic (ML_Syntax.print_range range)) ctxt;
    8.97 +                  in (decl #> tokenize range, ctxt') end
    8.98 +                else (K ([], [tok]), ctxt);
    8.99  
   8.100            val ctxt =
   8.101              (case opt_ctxt of
     9.1 --- a/src/Pure/ML/ml_lex.ML	Mon Dec 08 16:04:50 2014 +0100
     9.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Dec 08 22:42:12 2014 +0100
     9.3 @@ -9,12 +9,14 @@
     9.4    val keywords: string list
     9.5    datatype token_kind =
     9.6      Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
     9.7 -    Space | Comment | Error of string | EOF
     9.8 +    Space | Cartouche | Comment | Error of string | EOF
     9.9    eqtype token
    9.10    val stopper: token Scan.stopper
    9.11 +  val is_cartouche: token -> bool
    9.12    val is_regular: token -> bool
    9.13    val is_improper: token -> bool
    9.14    val set_range: Position.range -> token -> token
    9.15 +  val range_of: token -> Position.range
    9.16    val pos_of: token -> Position.T
    9.17    val end_pos_of: token -> Position.T
    9.18    val kind_of: token -> token_kind
    9.19 @@ -62,7 +64,7 @@
    9.20  
    9.21  datatype token_kind =
    9.22    Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
    9.23 -  Space | Comment | Error of string | EOF;
    9.24 +  Space | Cartouche | Comment | Error of string | EOF;
    9.25  
    9.26  datatype token = Token of Position.range * (token_kind * string);
    9.27  
    9.28 @@ -70,9 +72,10 @@
    9.29  (* position *)
    9.30  
    9.31  fun set_range range (Token (_, x)) = Token (range, x);
    9.32 +fun range_of (Token (range, _)) = range;
    9.33  
    9.34 -fun pos_of (Token ((pos, _), _)) = pos;
    9.35 -fun end_pos_of (Token ((_, pos), _)) = pos;
    9.36 +val pos_of = #1 o range_of;
    9.37 +val end_pos_of = #2 o range_of;
    9.38  
    9.39  
    9.40  (* stopper *)
    9.41 @@ -100,6 +103,9 @@
    9.42  fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x)
    9.43    | is_delimiter _ = false;
    9.44  
    9.45 +fun is_cartouche (Token (_, (Cartouche, _))) = true
    9.46 +  | is_cartouche _ = false;
    9.47 +
    9.48  fun is_regular (Token (_, (Error _, _))) = false
    9.49    | is_regular (Token (_, (EOF, _))) = false
    9.50    | is_regular _ = true;
    9.51 @@ -121,6 +127,9 @@
    9.52      Error msg => error msg
    9.53    | _ => content_of tok);
    9.54  
    9.55 +
    9.56 +(* flatten *)
    9.57 +
    9.58  fun flatten_content (tok :: (toks as tok' :: _)) =
    9.59        Symbol.escape (check_content_of tok) ::
    9.60          (if is_improper tok orelse is_improper tok' then flatten_content toks
    9.61 @@ -145,6 +154,7 @@
    9.62    | Char => (Markup.ML_char, "")
    9.63    | String => (if SML then Markup.SML_string else Markup.ML_string, "")
    9.64    | Space => (Markup.empty, "")
    9.65 +  | Cartouche => (Markup.ML_cartouche, "")
    9.66    | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
    9.67    | Error msg => (Markup.bad, msg)
    9.68    | EOF => (Markup.empty, "");
    9.69 @@ -284,11 +294,17 @@
    9.70      scan_ident >> token Ident ||
    9.71      scan_type_var >> token Type_Var));
    9.72  
    9.73 -val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;
    9.74 +val scan_sml = scan_ml >> Antiquote.Text;
    9.75 +
    9.76 +val scan_ml_antiq =
    9.77 +  Antiquote.scan_antiq >> Antiquote.Antiq ||
    9.78 +  Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) ||
    9.79 +  scan_ml >> Antiquote.Text;
    9.80  
    9.81  fun recover msg =
    9.82   (recover_char ||
    9.83    recover_string ||
    9.84 +  Symbol_Pos.recover_cartouche ||
    9.85    Symbol_Pos.recover_comment ||
    9.86    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
    9.87    >> (single o token (Error msg));
    9.88 @@ -307,7 +323,7 @@
    9.89            val pos2 = Position.advance Symbol.space pos1;
    9.90          in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
    9.91  
    9.92 -    val scan = if SML then scan_ml >> Antiquote.Text else scan_antiq;
    9.93 +    val scan = if SML then scan_sml else scan_ml_antiq;
    9.94      fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
    9.95        | check _ = ();
    9.96      val input =
    10.1 --- a/src/Pure/ML/ml_lex.scala	Mon Dec 08 16:04:50 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_lex.scala	Mon Dec 08 22:42:12 2014 +0100
    10.3 @@ -50,6 +50,7 @@
    10.4      val CHAR = Value("character")
    10.5      val STRING = Value("quoted string")
    10.6      val SPACE = Value("white space")
    10.7 +    val CARTOUCHE = Value("text cartouche")
    10.8      val COMMENT = Value("comment text")
    10.9      val ANTIQ = Value("antiquotation")
   10.10      val ANTIQ_START = Value("antiquotation: start")
   10.11 @@ -133,6 +134,15 @@
   10.12      }
   10.13  
   10.14  
   10.15 +    /* ML cartouche */
   10.16 +
   10.17 +    private val ml_cartouche: Parser[Token] =
   10.18 +      cartouche ^^ (x => Token(Kind.CARTOUCHE, x))
   10.19 +
   10.20 +    private def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
   10.21 +      cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.CARTOUCHE, x), c) }
   10.22 +
   10.23 +
   10.24      /* ML comment */
   10.25  
   10.26      private val ml_comment: Parser[Token] =
   10.27 @@ -145,10 +155,11 @@
   10.28      /* delimited token */
   10.29  
   10.30      private def delimited_token: Parser[Token] =
   10.31 -      ml_char | (ml_string | ml_comment)
   10.32 +      ml_char | (ml_string | (ml_cartouche | ml_comment))
   10.33  
   10.34      private val recover_delimited: Parser[Token] =
   10.35 -      (recover_ml_char | (recover_ml_string | recover_comment)) ^^ (x => Token(Kind.ERROR, x))
   10.36 +      (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^
   10.37 +        (x => Token(Kind.ERROR, x))
   10.38  
   10.39  
   10.40      private def other_token: Parser[Token] =
   10.41 @@ -246,8 +257,9 @@
   10.42        if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
   10.43        else
   10.44          ml_string_line(ctxt) |
   10.45 -          (ml_comment_line(ctxt) |
   10.46 -            (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
   10.47 +          (ml_cartouche_line(ctxt) |
   10.48 +            (ml_comment_line(ctxt) |
   10.49 +              (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))
   10.50      }
   10.51    }
   10.52  
    11.1 --- a/src/Pure/ML/ml_thms.ML	Mon Dec 08 16:04:50 2014 +0100
    11.2 +++ b/src/Pure/ML/ml_thms.ML	Mon Dec 08 22:42:12 2014 +0100
    11.3 @@ -42,16 +42,12 @@
    11.4  val _ = Theory.setup
    11.5    (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs)
    11.6      (fn _ => fn raw_srcs => fn ctxt =>
    11.7 -      let
    11.8 -        val i = serial ();
    11.9 -
   11.10 -        val (a, ctxt') = ctxt
   11.11 -          |> ML_Antiquotation.variant "attributes"
   11.12 -          ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs);
   11.13 -        val ml =
   11.14 -          ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
   11.15 -            string_of_int i ^ ";\n", "Isabelle." ^ a);
   11.16 -      in (K ml, ctxt') end));
   11.17 +      let val i = serial () in
   11.18 +        ctxt
   11.19 +        |> put_attributes (i, Attrib.check_attribs ctxt raw_srcs)
   11.20 +        |> ML_Context.value_decl "attributes"
   11.21 +            ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
   11.22 +      end));
   11.23  
   11.24  
   11.25  (* fact references *)
   11.26 @@ -59,7 +55,7 @@
   11.27  fun thm_binding kind is_single thms ctxt =
   11.28    let
   11.29      val initial = null (get_thmss ctxt);
   11.30 -    val (name, ctxt') = ML_Antiquotation.variant kind ctxt;
   11.31 +    val (name, ctxt') = ML_Context.variant kind ctxt;
   11.32      val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
   11.33  
   11.34      val ml_body = "Isabelle." ^ name;
    12.1 --- a/src/Pure/PIDE/markup.ML	Mon Dec 08 16:04:50 2014 +0100
    12.2 +++ b/src/Pure/PIDE/markup.ML	Mon Dec 08 22:42:12 2014 +0100
    12.3 @@ -99,6 +99,7 @@
    12.4    val ML_numeralN: string val ML_numeral: T
    12.5    val ML_charN: string val ML_char: T
    12.6    val ML_stringN: string val ML_string: T
    12.7 +  val ML_cartoucheN: string val ML_cartouche: T
    12.8    val ML_commentN: string val ML_comment: T
    12.9    val SML_stringN: string val SML_string: T
   12.10    val SML_commentN: string val SML_comment: T
   12.11 @@ -427,6 +428,7 @@
   12.12  val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
   12.13  val (ML_charN, ML_char) = markup_elem "ML_char";
   12.14  val (ML_stringN, ML_string) = markup_elem "ML_string";
   12.15 +val (ML_cartoucheN, ML_cartouche) = markup_elem "ML_cartouche";
   12.16  val (ML_commentN, ML_comment) = markup_elem "ML_comment";
   12.17  val (SML_stringN, SML_string) = markup_elem "SML_string";
   12.18  val (SML_commentN, SML_comment) = markup_elem "SML_comment";
    13.1 --- a/src/Pure/PIDE/markup.scala	Mon Dec 08 16:04:50 2014 +0100
    13.2 +++ b/src/Pure/PIDE/markup.scala	Mon Dec 08 22:42:12 2014 +0100
    13.3 @@ -241,6 +241,7 @@
    13.4    val ML_NUMERAL = "ML_numeral"
    13.5    val ML_CHAR = "ML_char"
    13.6    val ML_STRING = "ML_string"
    13.7 +  val ML_CARTOUCHE = "ML_cartouche"
    13.8    val ML_COMMENT = "ML_comment"
    13.9    val SML_STRING = "SML_string"
   13.10    val SML_COMMENT = "SML_comment"
    14.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Dec 08 16:04:50 2014 +0100
    14.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Dec 08 22:42:12 2014 +0100
    14.3 @@ -106,6 +106,7 @@
    14.4        ML_Lex.Kind.CHAR -> LITERAL2,
    14.5        ML_Lex.Kind.STRING -> LITERAL1,
    14.6        ML_Lex.Kind.SPACE -> NULL,
    14.7 +      ML_Lex.Kind.CARTOUCHE -> COMMENT4,
    14.8        ML_Lex.Kind.COMMENT -> COMMENT1,
    14.9        ML_Lex.Kind.ANTIQ -> NULL,
   14.10        ML_Lex.Kind.ANTIQ_START -> LITERAL4,
   14.11 @@ -727,6 +728,7 @@
   14.12        Markup.ML_NUMERAL -> inner_numeral_color,
   14.13        Markup.ML_CHAR -> inner_quoted_color,
   14.14        Markup.ML_STRING -> inner_quoted_color,
   14.15 +      Markup.ML_CARTOUCHE -> inner_cartouche_color,
   14.16        Markup.ML_COMMENT -> inner_comment_color,
   14.17        Markup.SML_STRING -> inner_quoted_color,
   14.18        Markup.SML_COMMENT -> inner_comment_color)