# HG changeset patch
# User wenzelm
# Date 1282210131 -7200
# Node ID 81ec258c4cd3f553954fe5972df2c967a36fc5aa
# Parent  e5eed57913d0545af276e7affbbc5e828e6ebeb0
Output_Position.report_text -- markup with potential "arguments";

diff -r e5eed57913d0 -r 81ec258c4cd3 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Thu Aug 19 11:26:07 2010 +0200
+++ b/src/Pure/context_position.ML	Thu Aug 19 11:28:51 2010 +0200
@@ -9,6 +9,7 @@
   val is_visible: Proof.context -> bool
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
+  val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
 
@@ -25,7 +26,9 @@
 val set_visible = Data.put;
 val restore_visible = set_visible o is_visible;
 
-fun report ctxt markup pos =
-  if is_visible ctxt then Position.report markup pos else ();
+fun report_text ctxt markup pos txt =
+  if is_visible ctxt then Position.report_text markup pos txt else ();
+
+fun report ctxt markup pos = report_text ctxt markup pos "";
 
 end;