1.1 --- a/src/Pure/General/pretty.ML	Wed Jul 11 17:47:48 2007 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Wed Jul 11 17:47:49 2007 +0200
     1.3 @@ -299,25 +299,21 @@
     1.4  
     1.5  (* special output *)
     1.6  
     1.7 -fun add_markup m add =
     1.8 -  let val (bg, en) = Markup.output m
     1.9 -  in Buffer.add bg #> add #> Buffer.add en end;
    1.10 -
    1.11  (*symbolic markup -- no formatting*)
    1.12  fun symbolic prt =
    1.13    let
    1.14 -    fun out (Block (m, [], _, _)) = add_markup m I
    1.15 +    fun out (Block (m, [], _, _)) = Buffer.markup m I
    1.16        | out (Block (m, prts, indent, _)) =
    1.17 -          add_markup m (add_markup (Markup.block indent) (fold out prts))
    1.18 +          Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
    1.19        | out (String (s, _)) = Buffer.add s
    1.20 -      | out (Break (false, wd)) = add_markup (Markup.break wd) (Buffer.add (output_spaces wd))
    1.21 -      | out (Break (true, _)) = add_markup Markup.fbreak (Buffer.add (output_spaces 1));
    1.22 +      | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
    1.23 +      | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
    1.24    in out prt Buffer.empty end;
    1.25  
    1.26  (*unformatted output*)
    1.27  fun unformatted prt =
    1.28    let
    1.29 -    fun fmt (Block (m, prts, _, _)) = add_markup m (fold fmt prts)
    1.30 +    fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
    1.31        | fmt (String (s, _)) = Buffer.add s
    1.32        | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
    1.33        | fmt (Break (true, _)) = Buffer.add (output_spaces 1);