diff -r 1c294d150ded -r 4c2547af5909 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Sep 17 15:51:11 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Sep 17 17:09:31 2010 +0200
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
   val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
@@ -29,9 +30,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun report_text ctxt markup pos txt =
-  if is_visible ctxt then Position.report_text markup pos txt else ();
+fun reported_text ctxt markup pos txt =
+  if is_visible ctxt then Position.reported_text markup pos txt else "";
 
+fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
 fun report ctxt markup pos = report_text ctxt markup pos "";
 
 end;