--- a/src/Pure/context_position.ML Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/context_position.ML Tue Sep 06 20:37:07 2011 +0200
@@ -14,6 +14,7 @@
val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
val report: Proof.context -> Position.T -> Markup.T -> unit
+ val reports: Proof.context -> Position.report list -> unit
end;
structure Context_Position: CONTEXT_POSITION =
@@ -35,4 +36,6 @@
fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
fun report ctxt pos markup = report_text ctxt pos markup "";
+fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
+
end;