# HG changeset patch
# User wenzelm
# Date 1218812635 -7200
# Node ID e4f8763b971b1bbcaf9b5eb644afbf3adce5a614
# Parent  a06f78f917e007619b8a3c29aaf76dbc041c8852
report antiquotation names;

diff -r a06f78f917e0 -r e4f8763b971b src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Aug 15 17:03:52 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Aug 15 17:03:55 2008 +0200
@@ -106,7 +106,8 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_parsers) name of
       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan => Args.context_syntax "ML antiquotation" (scan pos) src ctxt)
+    | SOME scan => (Position.report (Markup.ML_antiq name) pos;
+        Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
   end;
 
 end;