# HG changeset patch
# User wenzelm
# Date 1237751387 -3600
# Node ID 72980f8d7ee8174897e5ffe4acc1314e0fa1b8de
# Parent  3f3d1e218b64d3f9f8c0b80bb2e89fd1a61c9b9a
export report -- version that actually covers all cases;
export check_nesting;
simplified read (again);

diff -r 3f3d1e218b64 -r 72980f8d7ee8 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Mar 22 19:12:36 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Mar 22 20:49:47 2009 +0100
@@ -12,10 +12,11 @@
     Open of Position.T |
     Close of Position.T
   val is_text: 'a antiquote -> bool
+  val report: ('a -> unit) -> 'a antiquote -> unit
+  val check_nesting: 'a antiquote list -> unit
   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: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
-    Symbol_Pos.T list * Position.T -> 'a antiquote list
+  val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
 end;
 
 structure Antiquote: ANTIQUOTE =
@@ -33,6 +34,16 @@
   | is_text _ = false;
 
 
+(* report *)
+
+val report_antiq = Position.report Markup.antiq;
+
+fun report report_text (Text x) = report_text x
+  | report _ (Antiq (_, pos)) = report_antiq pos
+  | report _ (Open pos) = report_antiq pos
+  | report _ (Close pos) = report_antiq pos;
+
+
 (* check_nesting *)
 
 fun err_unbalanced pos =
@@ -83,12 +94,9 @@
 
 (* read *)
 
-fun read _ _ ([], _) = []
-  | read report scanner (syms, pos) =
-      (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
-        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));
+fun read (syms, pos) =
+  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
+    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 end;