# HG changeset patch # User wenzelm # Date 1394660464 -3600 # Node ID 1bc0bea908c396ca321ca3c06814194879d53437 # Parent 451d5b73f8cf1a58d64d8b20956b10a21aa73360 ML_Context.check_antiquotation still required; diff -r 451d5b73f8cf -r 1bc0bea908c3 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Wed Mar 12 21:58:48 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Wed Mar 12 22:41:04 2014 +0100 @@ -267,7 +267,7 @@ entity_antiqs no_check "" "inference" #> entity_antiqs no_check "isatt" "executable" #> entity_antiqs (K check_tool) "isatool" "tool" #> - entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #> + entity_antiqs (can o ML_Context.check_antiquotation) "" Markup.ML_antiquotationN #> entity_antiqs (K (is_action o #1)) "isatt" "action"); end; diff -r 451d5b73f8cf -r 1bc0bea908c3 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Wed Mar 12 21:58:48 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Wed Mar 12 22:41:04 2014 +0100 @@ -23,6 +23,7 @@ val get_stored_thm: unit -> thm val ml_store_thms: string * thm list -> unit val ml_store_thm: string * thm -> unit + val check_antiquotation: Proof.context -> xstring * Position.T -> string val print_antiquotations: Proof.context -> unit type decl = Proof.context -> string * string val antiquotation: binding -> 'a context_parser -> @@ -109,6 +110,9 @@ val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; +fun check_antiquotation ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt); + fun add_antiquotation name f thy = thy |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);