proper context for global data;

--- a/src/Doc/antiquote_setup.ML	Tue Feb 25 14:34:18 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Feb 25 14:56:58 2014 +0100
@@ -156,8 +156,6 @@
       val _ = List.app (Position.report pos) markup;
     in true end;
 
-fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
-
 fun check_tool (name, pos) =
   let
     fun tool dir =
@@ -213,18 +211,18 @@
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
   entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
   entity_antiqs (can o Method.check_name) "" "method" #>
-  entity_antiqs (thy_check Attrib.check) "" "attribute" #>
+  entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #>
   entity_antiqs no_check "" "fact" #>
   entity_antiqs no_check "" "variable" #>
   entity_antiqs no_check "" "case" #>
-  entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #>
-  entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #>
+  entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
+  entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
   entity_antiqs no_check "isatt" "setting" #>
   entity_antiqs no_check "isatt" "system option" #>
   entity_antiqs no_check "" "inference" #>
   entity_antiqs no_check "isatt" "executable" #>
   entity_antiqs (K check_tool) "isatool" "tool" #>
-  entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN;
+  entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
 
 end;
 

--- a/src/Pure/ML/ml_context.ML	Tue Feb 25 14:34:18 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Feb 25 14:56:58 2014 +0100
@@ -25,7 +25,7 @@
   val ml_store_thm: string * thm -> unit
   type antiq = Proof.context -> string * string
   val add_antiq: binding -> antiq context_parser -> theory -> theory
-  val check_antiq: theory -> xstring * Position.T -> string
+  val check_antiq: Proof.context -> xstring * Position.T -> string
   val trace_raw: Config.raw
   val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -107,16 +107,17 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
+val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of;
+
 fun add_antiq name scan thy = thy
   |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
 
-fun check_antiq thy = #1 o Name_Space.check (Context.Theory thy) (Antiq_Parsers.get thy);
+fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
 
 fun antiquotation src ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val ((xname, _), pos) = Args.dest_src src;
-    val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
+    val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos);
   in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
 
 

--- a/src/Pure/Thy/thy_output.ML	Tue Feb 25 14:34:18 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Feb 25 14:56:58 2014 +0100
@@ -14,8 +14,8 @@
   val modes: string Config.T
   val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
   val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
-  val check_command: theory -> xstring * Position.T -> string
-  val check_option: theory -> xstring * Position.T -> string
+  val check_command: Proof.context -> xstring * Position.T -> string
+  val check_option: Proof.context -> xstring * Position.T -> string
   val print_antiquotations: Proof.context -> unit
   val antiquotation: binding -> 'a context_parser ->
     ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
@@ -79,21 +79,23 @@
       Name_Space.merge_tables (options1, options2));
 );
 
+val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
+
 fun add_command name cmd thy = thy
   |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
 
 fun add_option name opt thy = thy
   |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
 
-fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy));
+fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
 
-fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy));
+fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
 fun command src state ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val ((xname, _), pos) = Args.dest_src src;
-    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
+    val (name, f) =
+      Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
   in
     f src state ctxt handle ERROR msg =>
       cat_error msg ("The error(s) above occurred in document antiquotation: " ^
@@ -102,14 +104,13 @@
 
 fun option ((xname, pos), s) ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
+    val (_, opt) =
+      Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   in opt s ctxt end;
 
 fun print_antiquotations ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val (commands, options) = Antiquotations.get thy;
+    val (commands, options) = get_antiquotations ctxt;
     val command_names = map #1 (Name_Space.extern_table ctxt commands);
     val option_names = map #1 (Name_Space.extern_table ctxt options);
   in