src/Pure/ML/ml_context.ML
changeset 27895 e4f8763b971b
parent 27878 1ba19c9edd18
child 28270 7ada24ebea94
equal deleted inserted replaced
27894:a06f78f917e0 27895:e4f8763b971b
   104 
   104 
   105 fun antiquotation src ctxt =
   105 fun antiquotation src ctxt =
   106   let val ((name, _), pos) = Args.dest_src src in
   106   let val ((name, _), pos) = Args.dest_src src in
   107     (case Symtab.lookup (! global_parsers) name of
   107     (case Symtab.lookup (! global_parsers) name of
   108       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   108       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   109     | SOME scan => Args.context_syntax "ML antiquotation" (scan pos) src ctxt)
   109     | SOME scan => (Position.report (Markup.ML_antiq name) pos;
       
   110         Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   110   end;
   111   end;
   111 
   112 
   112 end;
   113 end;
   113 
   114 
   114 
   115