equal
deleted
inserted
replaced
116 |
116 |
117 fun antiquotation src ctxt = |
117 fun antiquotation src ctxt = |
118 let val ((name, _), pos) = Args.dest_src src in |
118 let val ((name, _), pos) = Args.dest_src src in |
119 (case Symtab.lookup (! global_parsers) name of |
119 (case Symtab.lookup (! global_parsers) name of |
120 NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
120 NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
121 | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos; |
121 | SOME scan => |
|
122 (Context_Position.report ctxt pos (Markup.ML_antiq name); |
122 Args.context_syntax "ML antiquotation" (scan pos) src ctxt)) |
123 Args.context_syntax "ML antiquotation" (scan pos) src ctxt)) |
123 end; |
124 end; |
124 |
125 |
125 end; |
126 end; |
126 |
127 |