# HG changeset patch
# User wenzelm
# Date 1183917130 -7200
# Node ID 4b702ac388d691c5732bb407ceb68d565e03bee1
# Parent  d9f8aa7fe6b0ce62d66ec83b6d384cfa03c26834
symbolic output: avoid empty blocks, 1 space for fbreak;

diff -r d9f8aa7fe6b0 -r 4b702ac388d6 src/Pure/General/pretty.ML
--- 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*)