# 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 =