# HG changeset patch
# User wenzelm
# Date 1183826358 -7200
# Node ID 09120c2dd71fbfc4a0a5e502b843ea34a6584382
# Parent  f3e16ee56f327a229236f460ff6d135e425f6f33
added markup_chunks;

diff -r f3e16ee56f32 -r 09120c2dd71f src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Jul 07 18:39:17 2007 +0200
+++ b/src/Pure/General/pretty.ML	Sat Jul 07 18:39:18 2007 +0200
@@ -42,6 +42,7 @@
   val keyword: string -> T
   val command: string -> T
   val strs: string list -> T
+  val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
   val block_enclose: T * T -> T list -> T
@@ -254,7 +255,10 @@
 fun command name = markup (Markup.command name) [str name];
 
 val strs = block o breaks o map str;
-fun chunks prts = blk (0, fbreaks prts);
+
+fun markup_chunks m prts = markup m (fbreaks prts);
+val chunks = markup_chunks Markup.none;
+
 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
 fun block_enclose (p1, p2) ps = chunks [(block  o fbreaks) (p1 :: ps), p2];