# HG changeset patch
# User wenzelm
# Date 1364216641 -3600
# Node ID e768a64ee53a3a0be4f5e3d445188caa3e627836
# Parent  b4f7e6734acc8ee0fdc636147c781f186d664904
clarified text_fold vs. fbrk;

diff -r b4f7e6734acc -r e768a64ee53a src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Mar 25 13:37:44 2013 +0100
+++ b/src/Pure/General/pretty.ML	Mon Mar 25 14:04:01 2013 +0100
@@ -168,7 +168,12 @@
 val chunks = markup_chunks Markup.empty;
 
 fun chunks2 prts =
-  blk (0, flat (Library.separate [fbrk, fbrk] (map (single o mark Markup.text_fold) prts)));
+  (case try split_last prts of
+    NONE => blk (0, [])
+  | SOME (prefix, last) =>
+      blk (0,
+        maps (fn prt => [markup Markup.text_fold [prt, fbrk], fbrk]) prefix @
+        [mark Markup.text_fold last]));
 
 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];