(name mess cleanup)
authorhaftmann
Wed Sep 21 10:39:38 2005 +0200 (2005-09-21)
changeset 17542b588e06b6775
parent 17541 6a52083b71c3
child 17543 79cc33f5ed37
(name mess cleanup)
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Wed Sep 21 10:33:59 2005 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Wed Sep 21 10:39:38 2005 +0200
     1.3 @@ -205,10 +205,10 @@
     1.4  fun quote prt =
     1.5    blk (1, [str "\"", prt, str "\""]);
     1.6  
     1.7 -fun separate_pretty delim prts =
     1.8 +fun separate_pretty sep prts =
     1.9    prts
    1.10    |> map single
    1.11 -  |> separate [str delim, brk 1]
    1.12 +  |> separate [str sep, brk 1]
    1.13    |> List.concat;
    1.14  
    1.15  val commas = separate_pretty ",";
    1.16 @@ -223,7 +223,7 @@
    1.17  fun enclose lpar rpar prts =
    1.18    block (str lpar :: (prts @ [str rpar]));
    1.19  
    1.20 -fun gen_list delim lpar rpar prts = enclose lpar rpar (separate_pretty delim prts);
    1.21 +fun gen_list sep lpar rpar prts = enclose lpar rpar (separate_pretty sep prts);
    1.22  val list = gen_list ",";
    1.23  fun str_list lpar rpar strs = list lpar rpar (map str strs);
    1.24  fun big_list name prts = block (fbreaks (str name :: prts));