Markup.output;
authorwenzelm
Tue Jul 10 16:45:00 2007 +0200 (2007-07-10)
changeset 2369763e3b2e383dd
parent 23696 ff97a943681e
child 23698 af84f2f13d4d
Markup.output;
src/Pure/General/position.ML
     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;