equal
deleted
inserted
replaced
113 |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd); |
113 |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd); |
114 |
114 |
115 fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt); |
115 fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt); |
116 |
116 |
117 fun antiquotation src ctxt = |
117 fun antiquotation src ctxt = |
118 let val (src', scan) = Args.check_src (Context.Proof ctxt) (get_antiqs ctxt) src |
118 let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src |
119 in Args.context_syntax Markup.ML_antiquotationN scan src' ctxt end; |
119 in Args.syntax scan src' ctxt end; |
120 |
120 |
121 |
121 |
122 (* parsing and evaluation *) |
122 (* parsing and evaluation *) |
123 |
123 |
124 local |
124 local |