# HG changeset patch
# User wenzelm
# Date 1309189888 -7200
# Node ID aeabb735883a3ad23cff735ce962db83e4ba61d7
# Parent  2c55eac2e5a982972de3f37f1e3f5a36cfcc40c6
proper checking of @{ML_antiquotation};

diff -r 2c55eac2e5a9 -r aeabb735883a doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Jun 27 17:20:24 2011 +0200
+++ b/doc-src/antiquote_setup.ML	Mon Jun 27 17:51:28 2011 +0200
@@ -192,7 +192,9 @@
 val _ = entity_antiqs no_check "isatt" "executable";
 val _ = entity_antiqs (K check_tool) "isatt" "tool";
 val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
-val _ = entity_antiqs no_check "" "ML antiquotation";  (* FIXME proper check *)
+val _ =
+  entity_antiqs
+    (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) "" Markup.ML_antiquotationN;
 
 end;
 
diff -r 2c55eac2e5a9 -r aeabb735883a src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Jun 27 17:20:24 2011 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Jun 27 17:51:28 2011 +0200
@@ -25,6 +25,8 @@
   val ml_store_thm: string * thm -> unit
   type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
   val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
+  val intern_antiq: theory -> xstring -> string
+  val defined_antiq: theory -> string -> bool
   val trace_raw: Config.raw
   val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -112,6 +114,9 @@
     (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
       (name, scan) #> snd);
 
+val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
+val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
+
 fun antiquotation src ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;