src/Pure/General/position.ML
changeset 30669 6de7ef888aa3
parent 29307 3a0b38b7fbb4
child 31424 d30a867a86fb
--- 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 *)