# HG changeset patch
# User wenzelm
# Date 1217935898 -7200
# Node ID d2523b72ed44eff9b01589c9bc032d258d8cb01b
# Parent  0b22524c05e202a805aef1e0626fc11751d687cc
added report;

diff -r 0b22524c05e2 -r d2523b72ed44 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 05 13:31:36 2008 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 05 13:31:38 2008 +0200
@@ -27,6 +27,7 @@
   val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
   type range = T * T
   val encode_range: range -> T
+  val report: Markup.T -> T -> unit
 end;
 
 structure Position: POSITION =
@@ -131,4 +132,11 @@
     | SOME (m, n) => [(Markup.end_lineN, string_of_int m), (Markup.end_columnN, string_of_int n)])
   in Pos (count, props') end;
 
+
+(* report markup *)
+
+fun report markup pos =
+  if pos = none then ()
+  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
+
 end;