# HG changeset patch
# User wenzelm
# Date 760280436 -3600
# Node ID 3441647c8c90280a8cc803f2b1c636ac82609dc8
# Parent  967813b8a7bf8825a0e022bd0d41408da5e2f434
added strs, big_list, writeln;

diff -r 967813b8a7bf -r 3441647c8c90 src/Pure/Syntax/pretty.ML
--- a/src/Pure/Syntax/pretty.ML	Thu Feb 03 13:59:56 1994 +0100
+++ b/src/Pure/Syntax/pretty.ML	Thu Feb 03 14:00:36 1994 +0100
@@ -36,10 +36,13 @@
   val breaks: T list -> T list
   val fbreaks: T list -> T list
   val block: T list -> T
+  val strs: string list -> T
   val parents: string -> string -> T list -> T
   val list: string -> string -> T list -> T
   val str_list: string -> string -> string list -> T
+  val big_list: string -> T list -> T
   val string_of: T -> string
+  val writeln: T -> unit
   val str_of: T -> string
   val pprint: T -> pprint_args -> unit
   val setdepth: int -> unit
@@ -165,6 +168,8 @@
 
 fun block prts = blk (2, prts);
 
+val strs = block o breaks o (map str);
+
 fun parents lpar rpar prts =
   block (str lpar :: (prts @ [str rpar]));
 
@@ -174,6 +179,9 @@
 fun str_list lpar rpar strs =
   list lpar rpar (map str strs);
 
+fun big_list name prts =
+  block (fbreaks (str name :: prts));
+
 
 
 (*** Pretty printing with depth limitation ***)
@@ -193,6 +201,8 @@
 
 fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
 
+val writeln = writeln o string_of;
+
 
 (*Create a single flat string: no line breaking*)
 fun str_of prt =