symbolic output: avoid empty blocks, 1 space for fbreak;
authorwenzelm
Sun Jul 08 19:52:10 2007 +0200 (2007-07-08)
changeset 236594b702ac388d6
parent 23658 d9f8aa7fe6b0
child 23660 18765718cf62
symbolic output: avoid empty blocks, 1 space for fbreak;
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Sun Jul 08 19:52:08 2007 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Sun Jul 08 19:52:10 2007 +0200
     1.3 @@ -313,11 +313,12 @@
     1.4  (*symbolic markup -- no formatting*)
     1.5  fun symbolic prt =
     1.6    let
     1.7 -    fun out (Block (m, prts, indent, _)) =
     1.8 +    fun out (Block (m, [], _, _)) = add_markup m I
     1.9 +      | out (Block (m, prts, indent, _)) =
    1.10            add_markup m (add_markup (Markup.block indent) (fold out prts))
    1.11        | out (String (s, _)) = Buffer.add s
    1.12        | out (Break (false, wd)) = add_markup (Markup.break wd) (Buffer.add (output_spaces wd))
    1.13 -      | out (Break (true, _)) = add_markup Markup.fbreak I
    1.14 +      | out (Break (true, _)) = add_markup Markup.fbreak (Buffer.add (output_spaces 1));
    1.15    in out prt Buffer.empty end;
    1.16  
    1.17  (*unformatted output*)