ML_Context.check_antiquotation still required;
authorwenzelm
Wed Mar 12 22:41:04 2014 +0100 (2014-03-12)
changeset 560701bc0bea908c3
parent 56069 451d5b73f8cf
child 56071 2ffdedb0c044
ML_Context.check_antiquotation still required;
src/Doc/antiquote_setup.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Wed Mar 12 21:58:48 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Wed Mar 12 22:41:04 2014 +0100
     1.3 @@ -267,7 +267,7 @@
     1.4      entity_antiqs no_check "" "inference" #>
     1.5      entity_antiqs no_check "isatt" "executable" #>
     1.6      entity_antiqs (K check_tool) "isatool" "tool" #>
     1.7 -    entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #>
     1.8 +    entity_antiqs (can o ML_Context.check_antiquotation) "" Markup.ML_antiquotationN #>
     1.9      entity_antiqs (K (is_action o #1)) "isatt" "action");
    1.10  
    1.11  end;
     2.1 --- a/src/Pure/ML/ml_context.ML	Wed Mar 12 21:58:48 2014 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Wed Mar 12 22:41:04 2014 +0100
     2.3 @@ -23,6 +23,7 @@
     2.4    val get_stored_thm: unit -> thm
     2.5    val ml_store_thms: string * thm list -> unit
     2.6    val ml_store_thm: string * thm -> unit
     2.7 +  val check_antiquotation: Proof.context -> xstring * Position.T -> string
     2.8    val print_antiquotations: Proof.context -> unit
     2.9    type decl = Proof.context -> string * string
    2.10    val antiquotation: binding -> 'a context_parser ->
    2.11 @@ -109,6 +110,9 @@
    2.12  
    2.13  val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
    2.14  
    2.15 +fun check_antiquotation ctxt =
    2.16 +  #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
    2.17 +
    2.18  fun add_antiquotation name f thy = thy
    2.19    |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
    2.20