--- a/src/Pure/General/pretty.ML Sun Jul 08 19:52:08 2007 +0200
+++ b/src/Pure/General/pretty.ML Sun Jul 08 19:52:10 2007 +0200
@@ -313,11 +313,12 @@
(*symbolic markup -- no formatting*)
fun symbolic prt =
let
- fun out (Block (m, prts, indent, _)) =
+ fun out (Block (m, [], _, _)) = add_markup m I
+ | out (Block (m, prts, indent, _)) =
add_markup m (add_markup (Markup.block indent) (fold out prts))
| out (String (s, _)) = Buffer.add s
| out (Break (false, wd)) = add_markup (Markup.break wd) (Buffer.add (output_spaces wd))
- | out (Break (true, _)) = add_markup Markup.fbreak I
+ | out (Break (true, _)) = add_markup Markup.fbreak (Buffer.add (output_spaces 1));
in out prt Buffer.empty end;
(*unformatted output*)