proper checking of @{ML_antiquotation};
authorwenzelm
Mon Jun 27 17:51:28 2011 +0200 (2011-06-27)
changeset 43563aeabb735883a
parent 43562 2c55eac2e5a9
child 43564 9864182c6bad
proper checking of @{ML_antiquotation};
doc-src/antiquote_setup.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Jun 27 17:20:24 2011 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Jun 27 17:51:28 2011 +0200
     1.3 @@ -192,7 +192,9 @@
     1.4  val _ = entity_antiqs no_check "isatt" "executable";
     1.5  val _ = entity_antiqs (K check_tool) "isatt" "tool";
     1.6  val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
     1.7 -val _ = entity_antiqs no_check "" "ML antiquotation";  (* FIXME proper check *)
     1.8 +val _ =
     1.9 +  entity_antiqs
    1.10 +    (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) "" Markup.ML_antiquotationN;
    1.11  
    1.12  end;
    1.13  
     2.1 --- a/src/Pure/ML/ml_context.ML	Mon Jun 27 17:20:24 2011 +0200
     2.2 +++ b/src/Pure/ML/ml_context.ML	Mon Jun 27 17:51:28 2011 +0200
     2.3 @@ -25,6 +25,8 @@
     2.4    val ml_store_thm: string * thm -> unit
     2.5    type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
     2.6    val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
     2.7 +  val intern_antiq: theory -> xstring -> string
     2.8 +  val defined_antiq: theory -> string -> bool
     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 @@ -112,6 +114,9 @@
    2.13      (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
    2.14        (name, scan) #> snd);
    2.15  
    2.16 +val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
    2.17 +val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
    2.18 +
    2.19  fun antiquotation src ctxt =
    2.20    let
    2.21      val thy = Proof_Context.theory_of ctxt;