1.1 --- a/src/Pure/General/pretty.ML	Wed Sep 14 23:55:49 2005 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Thu Sep 15 07:35:38 2005 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    val strs: string list -> T
     1.5    val enclose: string -> string -> T list -> T
     1.6    val list: string -> string -> T list -> T
     1.7 +  val gen_list: string -> string -> string -> T list -> T
     1.8    val str_list: string -> string -> string list -> T
     1.9    val big_list: string -> T list -> T
    1.10    val chunks: T list -> T
    1.11 @@ -204,8 +205,13 @@
    1.12  fun quote prt =
    1.13    blk (1, [str "\"", prt, str "\""]);
    1.14  
    1.15 -fun commas prts =
    1.16 -  List.concat (separate [str ",", brk 1] (map (fn x => [x]) prts));
    1.17 +fun separate_pretty delim prts =
    1.18 +  prts
    1.19 +  |> map single
    1.20 +  |> separate [str delim, brk 1]
    1.21 +  |> List.concat;
    1.22 +
    1.23 +val commas = separate_pretty ",";
    1.24  
    1.25  fun breaks prts = separate (brk 1) prts;
    1.26  fun fbreaks prts = separate fbrk prts;
    1.27 @@ -217,7 +223,8 @@
    1.28  fun enclose lpar rpar prts =
    1.29    block (str lpar :: (prts @ [str rpar]));
    1.30  
    1.31 -fun list lpar rpar prts = enclose lpar rpar (commas prts);
    1.32 +fun gen_list delim lpar rpar prts = enclose lpar rpar (separate_pretty delim prts);
    1.33 +val list = gen_list ",";
    1.34  fun str_list lpar rpar strs = list lpar rpar (map str strs);
    1.35  fun big_list name prts = block (fbreaks (str name :: prts));
    1.36  fun chunks prts = blk (0, fbreaks prts);