tuned;
authorwenzelm
Tue Nov 06 14:30:53 2018 +0100 (6 months ago)
changeset 69247fc24fe912258
parent 69245 3e9f812c308c
child 69248 9f21381600e3
tuned;
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Mon Nov 05 23:15:58 2018 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Nov 06 14:30:53 2018 +0100
     1.3 @@ -326,10 +326,10 @@
     1.4  (*unformatted output*)
     1.5  fun unformatted prt =
     1.6    let
     1.7 -    fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
     1.8 -      | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd)
     1.9 -      | fmt (Str (s, _)) = Buffer.add s;
    1.10 -  in fmt prt Buffer.empty end;
    1.11 +    fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
    1.12 +      | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
    1.13 +      | out (Str (s, _)) = Buffer.add s;
    1.14 +  in out prt Buffer.empty end;
    1.15  
    1.16  
    1.17  (* output interfaces *)