--- a/src/Pure/General/pretty.ML Fri Jan 05 14:31:47 2007 +0100
+++ b/src/Pure/General/pretty.ML Fri Jan 05 14:31:48 2007 +0100
@@ -37,6 +37,7 @@
val breaks: T list -> T list
val fbreaks: T list -> T list
val block: T list -> T
+ val block_enclose: T * T -> T list -> T
val strs: string list -> T
val chunks: T list -> T
val chunks2: T list -> T
@@ -220,6 +221,7 @@
val strs = block o breaks o map str;
fun chunks prts = blk (0, fbreaks prts);
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];
fun quote prt = blk (1, [str "\"", prt, str "\""]);
fun backquote prt = blk (1, [str "`", prt, str "`"]);