# HG changeset patch
# User haftmann
# Date 1126762538 -7200
# Node ID 6ede71a506f5a5cc74ebfb864632d00aa06a40db
# Parent  56a3a4affedcb3561e7e2fb4c4c9ee3a0b9abe7f
added gen_list to Pretty module

diff -r 56a3a4affedc -r 6ede71a506f5 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 14 23:55:49 2005 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 15 07:35:38 2005 +0200
@@ -40,6 +40,7 @@
   val strs: string list -> T
   val enclose: string -> string -> T list -> T
   val list: string -> string -> T list -> T
+  val gen_list: string -> string -> string -> T list -> T
   val str_list: string -> string -> string list -> T
   val big_list: string -> T list -> T
   val chunks: T list -> T
@@ -204,8 +205,13 @@
 fun quote prt =
   blk (1, [str "\"", prt, str "\""]);
 
-fun commas prts =
-  List.concat (separate [str ",", brk 1] (map (fn x => [x]) prts));
+fun separate_pretty delim prts =
+  prts
+  |> map single
+  |> separate [str delim, brk 1]
+  |> List.concat;
+
+val commas = separate_pretty ",";
 
 fun breaks prts = separate (brk 1) prts;
 fun fbreaks prts = separate fbrk prts;
@@ -217,7 +223,8 @@
 fun enclose lpar rpar prts =
   block (str lpar :: (prts @ [str rpar]));
 
-fun list lpar rpar prts = enclose lpar rpar (commas prts);
+fun gen_list delim lpar rpar prts = enclose lpar rpar (separate_pretty delim prts);
+val list = gen_list ",";
 fun str_list lpar rpar strs = list lpar rpar (map str strs);
 fun big_list name prts = block (fbreaks (str name :: prts));
 fun chunks prts = blk (0, fbreaks prts);