proper context for global data;
authorwenzelm
Tue Feb 25 14:56:58 2014 +0100 (2014-02-25)
changeset 55743225a060e7445
parent 55742 a989bdaf8121
child 55744 4a4e5686e091
proper context for global data;
src/Doc/antiquote_setup.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Feb 25 14:34:18 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Feb 25 14:56:58 2014 +0100
     1.3 @@ -156,8 +156,6 @@
     1.4        val _ = List.app (Position.report pos) markup;
     1.5      in true end;
     1.6  
     1.7 -fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
     1.8 -
     1.9  fun check_tool (name, pos) =
    1.10    let
    1.11      fun tool dir =
    1.12 @@ -213,18 +211,18 @@
    1.13    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
    1.14    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
    1.15    entity_antiqs (can o Method.check_name) "" "method" #>
    1.16 -  entity_antiqs (thy_check Attrib.check) "" "attribute" #>
    1.17 +  entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #>
    1.18    entity_antiqs no_check "" "fact" #>
    1.19    entity_antiqs no_check "" "variable" #>
    1.20    entity_antiqs no_check "" "case" #>
    1.21 -  entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #>
    1.22 -  entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #>
    1.23 +  entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
    1.24 +  entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
    1.25    entity_antiqs no_check "isatt" "setting" #>
    1.26    entity_antiqs no_check "isatt" "system option" #>
    1.27    entity_antiqs no_check "" "inference" #>
    1.28    entity_antiqs no_check "isatt" "executable" #>
    1.29    entity_antiqs (K check_tool) "isatool" "tool" #>
    1.30 -  entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN;
    1.31 +  entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
    1.32  
    1.33  end;
    1.34  
     2.1 --- a/src/Pure/ML/ml_context.ML	Tue Feb 25 14:34:18 2014 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Tue Feb 25 14:56:58 2014 +0100
     2.3 @@ -25,7 +25,7 @@
     2.4    val ml_store_thm: string * thm -> unit
     2.5    type antiq = Proof.context -> string * string
     2.6    val add_antiq: binding -> antiq context_parser -> theory -> theory
     2.7 -  val check_antiq: theory -> xstring * Position.T -> string
     2.8 +  val check_antiq: Proof.context -> xstring * Position.T -> string
     2.9    val trace_raw: Config.raw
    2.10    val trace: bool Config.T
    2.11    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    2.12 @@ -107,16 +107,17 @@
    2.13    fun merge data : T = Name_Space.merge_tables data;
    2.14  );
    2.15  
    2.16 +val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of;
    2.17 +
    2.18  fun add_antiq name scan thy = thy
    2.19    |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
    2.20  
    2.21 -fun check_antiq thy = #1 o Name_Space.check (Context.Theory thy) (Antiq_Parsers.get thy);
    2.22 +fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
    2.23  
    2.24  fun antiquotation src ctxt =
    2.25    let
    2.26 -    val thy = Proof_Context.theory_of ctxt;
    2.27      val ((xname, _), pos) = Args.dest_src src;
    2.28 -    val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
    2.29 +    val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos);
    2.30    in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
    2.31  
    2.32  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Tue Feb 25 14:34:18 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Feb 25 14:56:58 2014 +0100
     3.3 @@ -14,8 +14,8 @@
     3.4    val modes: string Config.T
     3.5    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
     3.6    val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
     3.7 -  val check_command: theory -> xstring * Position.T -> string
     3.8 -  val check_option: theory -> xstring * Position.T -> string
     3.9 +  val check_command: Proof.context -> xstring * Position.T -> string
    3.10 +  val check_option: Proof.context -> xstring * Position.T -> string
    3.11    val print_antiquotations: Proof.context -> unit
    3.12    val antiquotation: binding -> 'a context_parser ->
    3.13      ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
    3.14 @@ -79,21 +79,23 @@
    3.15        Name_Space.merge_tables (options1, options2));
    3.16  );
    3.17  
    3.18 +val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
    3.19 +
    3.20  fun add_command name cmd thy = thy
    3.21    |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
    3.22  
    3.23  fun add_option name opt thy = thy
    3.24    |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
    3.25  
    3.26 -fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy));
    3.27 +fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
    3.28  
    3.29 -fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy));
    3.30 +fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
    3.31  
    3.32  fun command src state ctxt =
    3.33    let
    3.34 -    val thy = Proof_Context.theory_of ctxt;
    3.35      val ((xname, _), pos) = Args.dest_src src;
    3.36 -    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
    3.37 +    val (name, f) =
    3.38 +      Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
    3.39    in
    3.40      f src state ctxt handle ERROR msg =>
    3.41        cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    3.42 @@ -102,14 +104,13 @@
    3.43  
    3.44  fun option ((xname, pos), s) ctxt =
    3.45    let
    3.46 -    val thy = Proof_Context.theory_of ctxt;
    3.47 -    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
    3.48 +    val (_, opt) =
    3.49 +      Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
    3.50    in opt s ctxt end;
    3.51  
    3.52  fun print_antiquotations ctxt =
    3.53    let
    3.54 -    val thy = Proof_Context.theory_of ctxt;
    3.55 -    val (commands, options) = Antiquotations.get thy;
    3.56 +    val (commands, options) = get_antiquotations ctxt;
    3.57      val command_names = map #1 (Name_Space.extern_table ctxt commands);
    3.58      val option_names = map #1 (Name_Space.extern_table ctxt options);
    3.59    in