src/Pure/Thy/thy_output.ML
changeset 55743 225a060e7445
parent 55739 d8270c17b5be
child 55761 213b9811f59f
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Feb 25 14:34:18 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Feb 25 14:56:58 2014 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4    val modes: string Config.T
     1.5    val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
     1.6    val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
     1.7 -  val check_command: theory -> xstring * Position.T -> string
     1.8 -  val check_option: theory -> xstring * Position.T -> string
     1.9 +  val check_command: Proof.context -> xstring * Position.T -> string
    1.10 +  val check_option: Proof.context -> xstring * Position.T -> string
    1.11    val print_antiquotations: Proof.context -> unit
    1.12    val antiquotation: binding -> 'a context_parser ->
    1.13      ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
    1.14 @@ -79,21 +79,23 @@
    1.15        Name_Space.merge_tables (options1, options2));
    1.16  );
    1.17  
    1.18 +val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
    1.19 +
    1.20  fun add_command name cmd thy = thy
    1.21    |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
    1.22  
    1.23  fun add_option name opt thy = thy
    1.24    |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
    1.25  
    1.26 -fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy));
    1.27 +fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
    1.28  
    1.29 -fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy));
    1.30 +fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
    1.31  
    1.32  fun command src state ctxt =
    1.33    let
    1.34 -    val thy = Proof_Context.theory_of ctxt;
    1.35      val ((xname, _), pos) = Args.dest_src src;
    1.36 -    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
    1.37 +    val (name, f) =
    1.38 +      Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
    1.39    in
    1.40      f src state ctxt handle ERROR msg =>
    1.41        cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    1.42 @@ -102,14 +104,13 @@
    1.43  
    1.44  fun option ((xname, pos), s) ctxt =
    1.45    let
    1.46 -    val thy = Proof_Context.theory_of ctxt;
    1.47 -    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
    1.48 +    val (_, opt) =
    1.49 +      Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
    1.50    in opt s ctxt end;
    1.51  
    1.52  fun print_antiquotations ctxt =
    1.53    let
    1.54 -    val thy = Proof_Context.theory_of ctxt;
    1.55 -    val (commands, options) = Antiquotations.get thy;
    1.56 +    val (commands, options) = get_antiquotations ctxt;
    1.57      val command_names = map #1 (Name_Space.extern_table ctxt commands);
    1.58      val option_names = map #1 (Name_Space.extern_table ctxt options);
    1.59    in