src/Pure/General/position.ML
changeset 23697 63e3b2e383dd
parent 23673 67c748e5ae54
child 23720 d0d583c7a41f
--- 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;