src/Pure/General/position.ML
changeset 23697 63e3b2e383dd
parent 23673 67c748e5ae54
child 23720 d0d583c7a41f
     1.1 --- a/src/Pure/General/position.ML	Tue Jul 10 16:44:58 2007 +0200
     1.2 +++ b/src/Pure/General/position.ML	Tue Jul 10 16:45:00 2007 +0200
     1.3 @@ -65,7 +65,8 @@
     1.4    | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
     1.5  
     1.6  fun str_of (Pos (NONE, NONE)) = ""
     1.7 -  | str_of pos = " " ^ Pretty.string_of (Pretty.markup
     1.8 -        (Markup.properties (properties_of pos) Markup.position) [Pretty.str (print pos)]);
     1.9 +  | str_of pos = " " ^
    1.10 +      (Markup.output (Markup.properties (properties_of pos) Markup.position) |-> enclose)
    1.11 +        (print pos);
    1.12  
    1.13  end;