# HG changeset patch
# User wenzelm
# Date 1374096748 -7200
# Node ID 6651abced1069bdf39ba1400a2b8531f0ee8e22d
# Parent  f06b403a7dcdb54c1c951e9213fdfce9db7c8ddb
tuned signature;

diff -r f06b403a7dcd -r 6651abced106 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jul 17 21:48:21 2013 +0200
+++ b/src/Pure/General/pretty.ML	Wed Jul 17 23:32:28 2013 +0200
@@ -39,6 +39,7 @@
   val mark_str: Markup.T * string -> T
   val marks_str: Markup.T list * string -> T
   val item: T list -> T
+  val text_fold: T list -> T
   val command: string -> T
   val keyword: string -> T
   val text: string -> T list
@@ -159,6 +160,7 @@
 fun marks_str (ms, s) = fold_rev mark ms (str s);
 
 val item = markup Markup.item;
+val text_fold = markup Markup.text_fold;
 
 fun command name = mark_str (Markup.keyword1, name);
 fun keyword name = mark_str (Markup.keyword2, name);
@@ -167,16 +169,14 @@
 val paragraph = markup Markup.paragraph;
 val para = paragraph o text;
 
-fun markup_chunks m prts = markup m (fbreaks (map (mark Markup.text_fold) prts));
+fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
 val chunks = markup_chunks Markup.empty;
 
 fun chunks2 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]));
+      blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
 
 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];