added block_enclose
authorhaftmann
Fri, 05 Jan 2007 14:31:48 +0100
changeset 22019 0b7aff48622e
parent 22018 b00adaa1ef99
child 22020 e52aef4ab54b
added block_enclose
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 "`"]);