equal
deleted
inserted
replaced
101 type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context; |
101 type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context; |
102 |
102 |
103 structure Antiq_Parsers = Theory_Data |
103 structure Antiq_Parsers = Theory_Data |
104 ( |
104 ( |
105 type T = (Position.T -> antiq context_parser) Name_Space.table; |
105 type T = (Position.T -> antiq context_parser) Name_Space.table; |
106 val empty : T = Name_Space.empty_table Markup.ML_antiquotationN; |
106 val empty : T = Name_Space.empty_table Isabelle_Markup.ML_antiquotationN; |
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 |
119 fun antiquotation src ctxt = |
119 fun antiquotation src ctxt = |
120 let |
120 let |
121 val thy = Proof_Context.theory_of ctxt; |
121 val thy = Proof_Context.theory_of ctxt; |
122 val ((xname, _), pos) = Args.dest_src src; |
122 val ((xname, _), pos) = Args.dest_src src; |
123 val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos); |
123 val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos); |
124 in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end; |
124 in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end; |
125 |
125 |
126 |
126 |
127 (* parsing and evaluation *) |
127 (* parsing and evaluation *) |
128 |
128 |
129 local |
129 local |