src/Pure/ML/ml_context.ML
changeset 43560 d1650e3720fd
parent 42360 da8817d01e7c
child 43563 aeabb735883a
     1.1 --- a/src/Pure/ML/ml_context.ML	Mon Jun 27 15:03:55 2011 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Mon Jun 27 16:53:31 2011 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val ml_store_thms: string * thm list -> unit
     1.5    val ml_store_thm: string * thm -> unit
     1.6    type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
     1.7 -  val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
     1.8 +  val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
     1.9    val trace_raw: Config.raw
    1.10    val trace: bool Config.T
    1.11    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    1.12 @@ -99,29 +99,25 @@
    1.13  
    1.14  type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
    1.15  
    1.16 -local
    1.17 -
    1.18 -val global_parsers =
    1.19 -  Unsynchronized.ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
    1.20 +structure Antiq_Parsers = Theory_Data
    1.21 +(
    1.22 +  type T = (Position.T -> antiq context_parser) Name_Space.table;
    1.23 +  val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
    1.24 +  val extend = I;
    1.25 +  fun merge data : T = Name_Space.merge_tables data;
    1.26 +);
    1.27  
    1.28 -in
    1.29 -
    1.30 -fun add_antiq name scan = CRITICAL (fn () =>
    1.31 -  Unsynchronized.change global_parsers (fn tab =>
    1.32 -   (if not (Symtab.defined tab name) then ()
    1.33 -    else warning ("Redefined ML antiquotation: " ^ quote name);
    1.34 -    Symtab.update (name, scan) tab)));
    1.35 +fun add_antiq name scan thy = thy
    1.36 +  |> Antiq_Parsers.map
    1.37 +    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
    1.38 +      (name, scan) #> snd);
    1.39  
    1.40  fun antiquotation src ctxt =
    1.41 -  let val ((name, _), pos) = Args.dest_src src in
    1.42 -    (case Symtab.lookup (! global_parsers) name of
    1.43 -      NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
    1.44 -    | SOME scan =>
    1.45 -       (Context_Position.report ctxt pos (Markup.ML_antiq name);
    1.46 -        Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
    1.47 -  end;
    1.48 -
    1.49 -end;
    1.50 +  let
    1.51 +    val thy = Proof_Context.theory_of ctxt;
    1.52 +    val ((xname, _), pos) = Args.dest_src src;
    1.53 +    val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
    1.54 +  in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
    1.55  
    1.56  
    1.57  (* parsing and evaluation *)