src/Pure/Syntax/pretty.ML

   val quote: T -> T
   val commas: T list -> T list
   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
   val setmargin: int -> unit
 end;

 
 fun fbreaks prts = separate fbrk prts;
 
 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]));
 
 fun list lpar rpar prts =
   parents lpar rpar (commas prts);
 
 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 ***)
 

 
 fun prune dp e = if dp>0 then pruning dp e else e;
 
 
 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 =
   let