src/Pure/General/antiquote.ML
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30635 a7d175c48228
     1.1 --- a/src/Pure/General/antiquote.ML	Fri Mar 20 20:20:09 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Fri Mar 20 20:21:38 2009 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    val is_antiq: 'a antiquote -> bool
     1.5    val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
     1.6    val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
     1.7 -  val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
     1.8 +  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
     1.9      Symbol_Pos.T list * Position.T -> 'a antiquote list
    1.10  end;
    1.11  
    1.12 @@ -83,13 +83,12 @@
    1.13  
    1.14  (* read *)
    1.15  
    1.16 -fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    1.17 -  | report_antiq _ = ();
    1.18 -
    1.19 -fun read _ ([], _) = []
    1.20 -  | read scanner (syms, pos) =
    1.21 +fun read _ _ ([], _) = []
    1.22 +  | read report scanner (syms, pos) =
    1.23        (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
    1.24 -        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    1.25 +        SOME xs =>
    1.26 +         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
    1.27 +          check_nesting xs; xs)
    1.28        | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    1.29  
    1.30  end;