--- a/src/Pure/General/pretty.ML Sat Dec 08 14:42:22 2001 +0100
+++ b/src/Pure/General/pretty.ML Sat Dec 08 14:42:45 2001 +0100
@@ -46,6 +46,7 @@
val indent: int -> T -> T
val string_of: T -> string
val writeln: T -> unit
+ val writelns: T list -> unit
val str_of: T -> string
val pprint: T -> pprint_args -> unit
val setdepth: int -> unit
@@ -223,6 +224,7 @@
fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
val writeln = writeln o string_of;
+fun writelns [] = () | writelns es = writeln (chunks es);
(*Create a single flat string: no line breaking*)