--- 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;