# HG changeset patch
# User wenzelm
# Date 1392839589 -3600
# Node ID 517db8dd12c2c9d72ff704e09ee32b3a16d8795a
# Parent  8ae36527c2a6ebefecae44c3632d40b38134b439
tuned signature;

diff -r 8ae36527c2a6 -r 517db8dd12c2 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Wed Feb 19 20:07:31 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Wed Feb 19 20:53:09 2014 +0100
@@ -9,7 +9,8 @@
   type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
   datatype 'a antiquote = Text of 'a | Antiq of antiq
   val is_text: 'a antiquote -> bool
-  val reports_of: ('a -> Position.report_text list) ->
+  val antiq_reports: antiq -> Position.report list
+  val antiquote_reports: ('a -> Position.report_text list) ->
     'a antiquote list -> Position.report_text list
   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
   val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
@@ -30,11 +31,11 @@
 
 (* reports *)
 
-fun reports_of_antiq ((_, {start, stop, range = (pos, _)}): antiq) =
-  map (rpair "") [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
+fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
+  [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
 
-fun reports_of text =
-  maps (fn Text x => text x | Antiq antiq => reports_of_antiq antiq);
+fun antiquote_reports text =
+  maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
 
 
 (* scan *)
@@ -75,7 +76,7 @@
 
 fun read (syms, pos) =
   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
-    SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
+    SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
 
 end;
diff -r 8ae36527c2a6 -r 517db8dd12c2 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Feb 19 20:07:31 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Feb 19 20:53:09 2014 +0100
@@ -314,7 +314,7 @@
         |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
           (SOME (false, fn msg => recover msg >> map Antiquote.Text))
         |> Source.exhaust
-        |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
+        |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token))
         |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
   in input @ termination end;