1.1 --- a/src/Pure/General/antiquote.ML	Wed Feb 19 20:07:31 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Wed Feb 19 20:53:09 2014 +0100
     1.3 @@ -9,7 +9,8 @@
     1.4    type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
     1.5    datatype 'a antiquote = Text of 'a | Antiq of antiq
     1.6    val is_text: 'a antiquote -> bool
     1.7 -  val reports_of: ('a -> Position.report_text list) ->
     1.8 +  val antiq_reports: antiq -> Position.report list
     1.9 +  val antiquote_reports: ('a -> Position.report_text list) ->
    1.10      'a antiquote list -> Position.report_text list
    1.11    val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
    1.12    val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    1.13 @@ -30,11 +31,11 @@
    1.14  
    1.15  (* reports *)
    1.16  
    1.17 -fun reports_of_antiq ((_, {start, stop, range = (pos, _)}): antiq) =
    1.18 -  map (rpair "") [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
    1.19 +fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
    1.20 +  [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
    1.21  
    1.22 -fun reports_of text =
    1.23 -  maps (fn Text x => text x | Antiq antiq => reports_of_antiq antiq);
    1.24 +fun antiquote_reports text =
    1.25 +  maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
    1.26  
    1.27  
    1.28  (* scan *)
    1.29 @@ -75,7 +76,7 @@
    1.30  
    1.31  fun read (syms, pos) =
    1.32    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    1.33 -    SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
    1.34 +    SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
    1.35    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    1.36  
    1.37  end;

     2.1 --- a/src/Pure/ML/ml_lex.ML	Wed Feb 19 20:07:31 2014 +0100
     2.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Feb 19 20:53:09 2014 +0100
     2.3 @@ -314,7 +314,7 @@
     2.4          |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
     2.5            (SOME (false, fn msg => recover msg >> map Antiquote.Text))
     2.6          |> Source.exhaust
     2.7 -        |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
     2.8 +        |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token))
     2.9          |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
    2.10    in input @ termination end;
    2.11