symbolic output: avoid empty blocks, 1 space for fbreak;

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