# HG changeset patch
# User wenzelm
# Date 1184078700 -7200
# Node ID 63e3b2e383ddf44e574cb87a648d579b1b223fd0
# Parent  ff97a943681e18489d628fabc619a7040054a9b9
Markup.output;

diff -r ff97a943681e -r 63e3b2e383dd src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Jul 10 16:44:58 2007 +0200
+++ b/src/Pure/General/position.ML	Tue Jul 10 16:45:00 2007 +0200
@@ -65,7 +65,8 @@
   | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
 
 fun str_of (Pos (NONE, NONE)) = ""
-  | str_of pos = " " ^ Pretty.string_of (Pretty.markup
-        (Markup.properties (properties_of pos) Markup.position) [Pretty.str (print pos)]);
+  | str_of pos = " " ^
+      (Markup.output (Markup.properties (properties_of pos) Markup.position) |-> enclose)
+        (print pos);
 
 end;