# HG changeset patch
# User wenzelm
# Date 1309186411 -7200
# Node ID d1650e3720fdd52905bfcfc82bf3412f396ad7e0
# Parent  c1966f3221059c9a5d028d1b2f5c7d3ee4e9509d
ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;

diff -r c1966f322105 -r d1650e3720fd src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/FOL/FOL.thy	Mon Jun 27 16:53:31 2011 +0200
@@ -177,12 +177,15 @@
   val hyp_subst_tacs = [hyp_subst_tac]
 );
 
-ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
-
 structure Basic_Classical: BASIC_CLASSICAL = Cla;
 open Basic_Classical;
 *}
 
+setup {*
+  ML_Antiquote.value @{binding claset}
+    (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())")
+*}
+
 setup Cla.setup
 
 (*Propositional rules*)
diff -r c1966f322105 -r d1650e3720fd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/HOL/HOL.thy	Mon Jun 27 16:53:31 2011 +0200
@@ -853,9 +853,11 @@
 
 structure Basic_Classical: BASIC_CLASSICAL = Classical; 
 open Basic_Classical;
+*}
 
-ML_Antiquote.value "claset"
-  (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
+setup {*
+  ML_Antiquote.value @{binding claset}
+    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())")
 *}
 
 setup Classical.setup
diff -r c1966f322105 -r d1650e3720fd src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/General/markup.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -72,7 +72,7 @@
   val ML_sourceN: string val ML_source: T
   val doc_sourceN: string val doc_source: T
   val antiqN: string val antiq: T
-  val ML_antiqN: string val ML_antiq: string -> T
+  val ML_antiquotationN: string
   val doc_antiqN: string val doc_antiq: string -> T
   val keyword_declN: string val keyword_decl: string -> T
   val command_declN: string val command_decl: string -> string -> T
@@ -266,7 +266,7 @@
 val (doc_sourceN, doc_source) = markup_elem "doc_source";
 
 val (antiqN, antiq) = markup_elem "antiq";
-val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
+val ML_antiquotationN = "ML antiquotation";
 val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
 
 
diff -r c1966f322105 -r d1650e3720fd src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/General/markup.scala	Mon Jun 27 16:53:31 2011 +0200
@@ -189,7 +189,7 @@
   val DOC_SOURCE = "doc_source"
 
   val ANTIQ = "antiq"
-  val ML_ANTIQ = "ML_antiq"
+  val ML_ANTIQUOTATION = "ML antiquotation"
   val DOC_ANTIQ = "doc_antiq"
 
 
diff -r c1966f322105 -r d1650e3720fd src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/General/name_space.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -50,7 +50,7 @@
   val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
   val alias: naming -> binding -> string -> T -> T
   type 'a table = T * 'a Symtab.table
-  val check: Proof.context -> 'a table -> xstring * Position.T -> string
+  val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
   val get: 'a table -> string -> 'a
   val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
@@ -383,15 +383,15 @@
 
 
 
-(** name spaces coupled with symbol tables **)
+(** name space coupled with symbol table **)
 
 type 'a table = T * 'a Symtab.table;
 
 fun check ctxt (space, tab) (xname, pos) =
   let val name = intern space xname in
-    if Symtab.defined tab name
-    then (Context_Position.report ctxt pos (markup space name); name)
-    else error (undefined (kind_of space) name ^ Position.str_of pos)
+    (case Symtab.lookup tab name of
+      SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
+    | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
   end;
 
 fun get (space, tab) name =
diff -r c1966f322105 -r d1650e3720fd src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -303,8 +303,12 @@
   Proof.goal (Toplevel.proof_of (diag_state ()))
     handle Toplevel.UNDEF => error "No goal present";
 
-val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()");
-val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
+val _ =
+  Context.>> (Context.map_theory
+   (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
+      (Scan.succeed "Isar_Cmd.diag_state ()") #>
+    ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
+      (Scan.succeed "Isar_Cmd.diag_goal ()")));
 
 
 (* present draft files *)
diff -r c1966f322105 -r d1650e3720fd src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -6,11 +6,11 @@
 
 signature ML_ANTIQUOTE =
 sig
-  val macro: string -> Proof.context context_parser -> unit
   val variant: string -> Proof.context -> string * Proof.context
-  val inline: string -> string context_parser -> unit
-  val declaration: string -> string -> string context_parser -> unit
-  val value: string -> string context_parser -> unit
+  val macro: binding -> Proof.context context_parser -> theory -> theory
+  val inline: binding -> string context_parser -> theory -> theory
+  val declaration: string -> binding -> string context_parser -> theory -> theory
+  val value: binding -> string context_parser -> theory -> theory
 end;
 
 structure ML_Antiquote: ML_ANTIQUOTE =
@@ -46,7 +46,8 @@
 fun declaration kind name scan = ML_Context.add_antiq name
   (fn _ => scan >> (fn s => fn background =>
     let
-      val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
+      val (a, background') =
+        variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background;
       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
       val body = "Isabelle." ^ a;
     in (K (env, body), background') end));
@@ -57,48 +58,55 @@
 
 (** misc antiquotations **)
 
-val _ = inline "assert"
-  (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")");
+val _ = Context.>> (Context.map_theory
 
-val _ = inline "make_string" (Scan.succeed ml_make_string);
+ (inline (Binding.name "assert")
+    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
-val _ = value "binding"
-  (Scan.lift (Parse.position Args.name)
-    >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
+  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
 
-val _ = value "theory"
-  (Scan.lift Args.name >> (fn name =>
-    "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
-  || Scan.succeed "ML_Context.the_global_context ()");
+  value (Binding.name "binding")
+    (Scan.lift (Parse.position Args.name)
+      >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
 
-val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
+  value (Binding.name "theory")
+    (Scan.lift Args.name >> (fn name =>
+      "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
+    || Scan.succeed "ML_Context.the_global_context ()") #>
 
-val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
-val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
-val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
+  value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
 
-val _ = macro "let" (Args.context --
-  Scan.lift
-    (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
-    >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt)));
+  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
+  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
 
-val _ = macro "note" (Args.context :|-- (fn ctxt =>
-  Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
-    ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
-  >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt))));
+  macro (Binding.name "let")
+    (Args.context --
+      Scan.lift
+        (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
+        >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
 
-val _ = value "ctyp" (Args.typ >> (fn T =>
-  "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
+  macro (Binding.name "note")
+    (Args.context :|-- (fn ctxt =>
+      Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
+        >> (fn ((a, srcs), ths) =>
+          ((a, map (Attrib.attribute (Proof_Context.theory_of ctxt)) srcs), [(ths, [])])))
+      >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
 
-val _ = value "cterm" (Args.term >> (fn t =>
-  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
+  value (Binding.name "ctyp") (Args.typ >> (fn T =>
+    "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
 
-val _ = value "cprop" (Args.prop >> (fn t =>
-  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
+  value (Binding.name "cterm") (Args.term >> (fn t =>
+  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
 
-val _ = value "cpat"
-  (Args.context -- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
-    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
+  value (Binding.name "cprop") (Args.prop >> (fn t =>
+  "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+
+  value (Binding.name "cpat")
+    (Args.context --
+      Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
+        "Thm.cterm_of (ML_Context.the_global_context ()) " ^
+          ML_Syntax.atomic (ML_Syntax.print_term t)))));
 
 
 (* type classes *)
@@ -108,11 +116,13 @@
   |> syn ? Lexicon.mark_class
   |> ML_Syntax.print_string);
 
-val _ = inline "class" (class false);
-val _ = inline "class_syntax" (class true);
+val _ = Context.>> (Context.map_theory
+ (inline (Binding.name "class") (class false) #>
+  inline (Binding.name "class_syntax") (class true) #>
 
-val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
-  ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
+  inline (Binding.name "sort")
+    (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
 
 
 (* type constructors *)
@@ -128,10 +138,15 @@
         | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
     in ML_Syntax.print_string res end);
 
-val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
-val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
-val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
-val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c));
+val _ = Context.>> (Context.map_theory
+ (inline (Binding.name "type_name")
+    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
+  inline (Binding.name "type_abbrev")
+    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
+  inline (Binding.name "nonterminal")
+    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
+  inline (Binding.name "type_syntax")
+    (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
 
 
 (* constants *)
@@ -144,25 +159,28 @@
         handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
     in ML_Syntax.print_string res end);
 
-val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
-val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
-val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c));
+val _ = Context.>> (Context.map_theory
+ (inline (Binding.name "const_name")
+    (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #>
+  inline (Binding.name "const_abbrev")
+    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
+  inline (Binding.name "const_syntax")
+    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
 
+  inline (Binding.name "syntax_const")
+    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
+      then ML_Syntax.print_string c
+      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #>
 
-val _ = inline "syntax_const"
-  (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
-    if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
-    then ML_Syntax.print_string c
-    else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
-
-val _ = inline "const"
-  (Args.context -- Scan.lift Args.name_source -- Scan.optional
-      (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
-    >> (fn ((ctxt, raw_c), Ts) =>
-      let
-        val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
-        val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
-      in ML_Syntax.atomic (ML_Syntax.print_term const) end));
+  inline (Binding.name "const")
+    (Args.context -- Scan.lift Args.name_source -- Scan.optional
+        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+      >> (fn ((ctxt, raw_c), Ts) =>
+        let
+          val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
+          val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
+        in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
 
 end;
 
diff -r c1966f322105 -r d1650e3720fd src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -24,7 +24,7 @@
   val ml_store_thms: string * thm list -> unit
   val ml_store_thm: string * thm -> unit
   type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
-  val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
+  val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
   val trace_raw: Config.raw
   val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -99,29 +99,25 @@
 
 type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
 
-local
+structure Antiq_Parsers = Theory_Data
+(
+  type T = (Position.T -> antiq context_parser) Name_Space.table;
+  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
+  val extend = I;
+  fun merge data : T = Name_Space.merge_tables data;
+);
 
-val global_parsers =
-  Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
-
-in
-
-fun add_antiq name scan = CRITICAL (fn () =>
-  Unsynchronized.change global_parsers (fn tab =>
-   (if not (Symtab.defined tab name) then ()
-    else warning ("Redefined ML antiquotation: " ^ quote name);
-    Symtab.update (name, scan) tab)));
+fun add_antiq name scan thy = thy
+  |> Antiq_Parsers.map
+    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
+      (name, scan) #> snd);
 
 fun antiquotation src ctxt =
-  let val ((name, _), pos) = Args.dest_src src in
-    (case Symtab.lookup (! global_parsers) name of
-      NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan =>
-       (Context_Position.report ctxt pos (Markup.ML_antiq name);
-        Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
-  end;
-
-end;
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val ((xname, _), pos) = Args.dest_src src;
+    val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
+  in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
 
 
 (* parsing and evaluation *)
diff -r c1966f322105 -r d1650e3720fd src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/ML/ml_thms.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -33,7 +33,7 @@
 
 (* fact references *)
 
-fun thm_antiq kind scan = ML_Context.add_antiq kind
+fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind)
   (fn _ => scan >> (fn ths => fn background =>
     let
       val i = serial ();
@@ -42,8 +42,10 @@
       val ml = (thm_bind kind a i, "Isabelle." ^ a);
     in (K ml, background') end));
 
-val _ = thm_antiq "thm" (Attrib.thm >> single);
-val _ = thm_antiq "thms" Attrib.thms;
+val _ =
+  Context.>> (Context.map_theory
+   (thm_antiq "thm" (Attrib.thm >> single) #>
+    thm_antiq "thms" Attrib.thms));
 
 
 (* ad-hoc goals *)
@@ -52,25 +54,27 @@
 val by = Args.$$$ "by";
 val goal = Scan.unless (by || and_) Args.name;
 
-val _ = ML_Context.add_antiq "lemma"
-  (fn _ => Args.context -- Args.mode "open" --
-      Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
-        (by |-- Method.parse -- Scan.option Method.parse)) >>
-    (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
-      let
-        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
-        val i = serial ();
-        val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
-        fun after_qed res goal_ctxt =
-          put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
-        val ctxt' = ctxt
-          |> Proof.theorem NONE after_qed propss
-          |> Proof.global_terminal_proof methods;
-        val (a, background') = background
-          |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
-        val ml =
-          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
-      in (K ml, background') end));
+val _ =
+  Context.>> (Context.map_theory
+   (ML_Context.add_antiq (Binding.name "lemma")
+    (fn _ => Args.context -- Args.mode "open" --
+        Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
+          (by |-- Method.parse -- Scan.option Method.parse)) >>
+      (fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
+        let
+          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+          val i = serial ();
+          val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
+          fun after_qed res goal_ctxt =
+            put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt;
+          val ctxt' = ctxt
+            |> Proof.theorem NONE after_qed propss
+            |> Proof.global_terminal_proof methods;
+          val (a, background') = background
+            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
+          val ml =
+            (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
+        in (K ml, background') end))));
 
 end;
 
diff -r c1966f322105 -r d1650e3720fd src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Pure/simplifier.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -139,8 +139,9 @@
 fun map_simpset f = Context.proof_map (map_ss f);
 fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
 
-val _ = ML_Antiquote.value "simpset"
-  (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
+val _ = Context.>> (Context.map_theory
+  (ML_Antiquote.value (Binding.name "simpset")
+    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())")));
 
 
 (* global simpset *)
@@ -158,15 +159,16 @@
 
 (* get simprocs *)
 
-fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt);
+fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ =
-  ML_Antiquote.value "simproc"
-    (Args.context -- Scan.lift (Parse.position Args.name)
-      >> (fn (ctxt, name) =>
-        "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
-          ML_Syntax.print_string (check_simproc ctxt name)));
+  Context.>> (Context.map_theory
+   (ML_Antiquote.value (Binding.name "simproc")
+      (Args.context -- Scan.lift (Parse.position Args.name)
+        >> (fn (ctxt, name) =>
+          "Simplifier.the_simproc (ML_Context.the_local_context ()) " ^
+            ML_Syntax.print_string (check_simproc ctxt name)))));
 
 
 (* define simprocs *)
diff -r c1966f322105 -r d1650e3720fd src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon Jun 27 16:53:31 2011 +0200
@@ -336,7 +336,9 @@
 
 (** Isar setup **)
 
-val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
+val _ =
+  Context.>> (Context.map_theory
+    (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
 
 local
 
diff -r c1966f322105 -r d1650e3720fd src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 27 15:03:55 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 27 16:53:31 2011 +0200
@@ -114,7 +114,8 @@
     Map(
       Markup.CLASS -> get_color("red"),
       Markup.TYPE -> get_color("black"),
-      Markup.CONSTANT -> get_color("black"))
+      Markup.CONSTANT -> get_color("black"),
+      Markup.ML_ANTIQUOTATION -> get_color("black"))
 
   private val text_colors: Map[String, Color] =
     Map(