--- a/src/Pure/General/position.ML Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/General/position.ML Sun Apr 03 21:59:33 2011 +0200
@@ -34,6 +34,8 @@
val reported_text: T -> Markup.T -> string -> string
val report_text: T -> Markup.T -> string -> unit
val report: T -> Markup.T -> unit
+ type reports = (T * Markup.T) list
+ val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
val str_of: T -> string
type range = T * T
val no_range: range
@@ -155,6 +157,13 @@
fun report_text pos markup txt = Output.report (reported_text pos markup txt);
fun report pos markup = report_text pos markup "";
+type reports = (T * Markup.T) list;
+
+fun reports _ [] _ _ = ()
+ | reports (r: reports Unsynchronized.ref) ps markup x =
+ let val ms = markup x
+ in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
+
(* str_of *)