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*)