107 val extend = I; |
107 val extend = I; |
108 fun merge data : T = Name_Space.merge_tables data; |
108 fun merge data : T = Name_Space.merge_tables data; |
109 ); |
109 ); |
110 |
110 |
111 fun add_antiq name scan thy = thy |
111 fun add_antiq name scan thy = thy |
112 |> Antiq_Parsers.map |
112 |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd); |
113 (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy) |
|
114 (name, scan) #> snd); |
|
115 |
113 |
116 val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get; |
114 val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get; |
117 val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get; |
115 val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get; |
118 |
116 |
119 fun antiquotation src ctxt = |
117 fun antiquotation src ctxt = |
120 let |
118 let |
121 val thy = Proof_Context.theory_of ctxt; |
119 val thy = Proof_Context.theory_of ctxt; |
122 val ((xname, _), pos) = Args.dest_src src; |
120 val ((xname, _), pos) = Args.dest_src src; |
123 val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos); |
121 val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos); |
124 in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end; |
122 in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end; |
125 |
123 |
126 |
124 |
127 (* parsing and evaluation *) |
125 (* parsing and evaluation *) |
128 |
126 |