# HG changeset patch
# User wenzelm
# Date 1237576898 -3600
# Node ID b22d35d9ef284696bdccf10889134f3e08d16e08
# Parent  cb6421b6a18f7636762d85fb18140ef2fd42db68
Antiquote.read: argument for reporting text;

diff -r cb6421b6a18f -r b22d35d9ef28 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Mar 20 20:20:09 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Fri Mar 20 20:21:38 2009 +0100
@@ -14,7 +14,7 @@
   val is_antiq: 'a antiquote -> bool
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
-  val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
+  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
     Symbol_Pos.T list * Position.T -> 'a antiquote list
 end;
 
@@ -83,13 +83,12 @@
 
 (* read *)
 
-fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
-  | report_antiq _ = ();
-
-fun read _ ([], _) = []
-  | read scanner (syms, pos) =
+fun read _ _ ([], _) = []
+  | read report scanner (syms, pos) =
       (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
-        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
+        SOME xs =>
+         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
+          check_nesting xs; xs)
       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 end;
diff -r cb6421b6a18f -r b22d35d9ef28 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Mar 20 20:20:09 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Fri Mar 20 20:21:38 2009 +0100
@@ -117,7 +117,7 @@
     else if T.is_kind T.Verbatim tok then
       let
         val (txt, pos) = T.source_position_of tok;
-        val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+        val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else output_syms s
diff -r cb6421b6a18f -r b22d35d9ef28 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Mar 20 20:20:09 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Mar 20 20:21:38 2009 +0100
@@ -156,7 +156,7 @@
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+    val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   in
     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)