src/Pure/General/position.ML

--- a/src/Pure/General/position.ML	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 31 23:28:21 2010 +0200
@@ -27,6 +27,7 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
+  val report_markup: T -> Markup.T
   val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
@@ -125,6 +126,8 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
+fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+
 fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
   else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);