(name mess cleanup)
authorhaftmann
Wed, 21 Sep 2005 10:39:38 +0200
changeset 17542 b588e06b6775
parent 17541 6a52083b71c3
child 17543 79cc33f5ed37
(name mess cleanup)
src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 21 10:33:59 2005 +0200
+++ b/src/Pure/General/pretty.ML	Wed Sep 21 10:39:38 2005 +0200
@@ -205,10 +205,10 @@
 fun quote prt =
   blk (1, [str "\"", prt, str "\""]);
 
-fun separate_pretty delim prts =
+fun separate_pretty sep prts =
   prts
   |> map single
-  |> separate [str delim, brk 1]
+  |> separate [str sep, brk 1]
   |> List.concat;
 
 val commas = separate_pretty ",";
@@ -223,7 +223,7 @@
 fun enclose lpar rpar prts =
   block (str lpar :: (prts @ [str rpar]));
 
-fun gen_list delim lpar rpar prts = enclose lpar rpar (separate_pretty delim prts);
+fun gen_list sep lpar rpar prts = enclose lpar rpar (separate_pretty sep 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));