# HG changeset patch
# User wenzelm
# Date 1218738578 -7200
# Node ID 4ab10bfe8a7f65fb8b4977f28b109fc9fff63a6a
# Parent  67d14d7c71431de008c4bf4fe9639ae6bb9cb75d
report antiquotations;

diff -r 67d14d7c7143 -r 4ab10bfe8a7f src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Thu Aug 14 20:29:37 2008 +0200
+++ b/src/Pure/Isar/antiquote.ML	Thu Aug 14 20:29:38 2008 +0200
@@ -82,10 +82,13 @@
 
 (* read *)
 
+fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
+  | report_antiq _ = ();
+
 fun read ([], _) = []
   | read (syms, pos) =
       (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
-        SOME xs => (check_nesting xs; xs)
+        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));