# HG changeset patch
# User wenzelm
# Date 1237825231 -3600
# Node ID 6de7ef888aa3b7a1a2a820ba639cdb460b5a39e4
# Parent  df8a3c2fd5a214c25b5943f57910a326c059d134
added report_text -- status messages with text body;

diff -r df8a3c2fd5a2 -r 6de7ef888aa3 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Mar 23 15:33:35 2009 +0100
+++ b/src/Pure/General/position.ML	Mon Mar 23 17:20:31 2009 +0100
@@ -24,6 +24,7 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
+  val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
   type range = T * T
@@ -121,9 +122,11 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
-fun report markup (pos as Pos (count, _)) =
+fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
-  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
+  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+
+fun report markup pos = report_text markup pos "";
 
 
 (* str_of *)