# HG changeset patch
# User haftmann
# Date 1168003908 -3600
# Node ID 0b7aff48622e1996ba82637a2cbc41cd68d282cf
# Parent  b00adaa1ef990e8c8f115d0be81152bb0e387d2d
added block_enclose

diff -r b00adaa1ef99 -r 0b7aff48622e src/Pure/General/pretty.ML
--- 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 "`"]);