private version of commas, cf. printmode

--- a/src/Tools/Code/code_ml.ML	Thu Aug 26 12:20:34 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 12:30:43 2010 +0200
@@ -489,7 +489,7 @@
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
-                (Pretty.block o Pretty.commas)
+                (Pretty.block o commas)
                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
                 str "->",
                 print_term is_pseudo_fun some_thm vars NOBR t
@@ -535,7 +535,7 @@
                       :: Pretty.brk 1
                       :: str "match"
                       :: Pretty.brk 1
-                      :: (Pretty.block o Pretty.commas) dummy_parms
+                      :: (Pretty.block o commas) dummy_parms
                       :: Pretty.brk 1
                       :: str "with"
                       :: Pretty.brk 1
@@ -813,7 +813,7 @@
         ) stmts
       #>> (split_list #> apsnd (map_filter I
         #> (fn [] => error ("Datatype block without data statement: "
-                  ^ (commas o map (labelled_name o fst)) stmts)
+                  ^ (Library.commas o map (labelled_name o fst)) stmts)
              | stmts => ML_Datas stmts)));
     fun add_class stmts =
       fold_map
@@ -828,7 +828,7 @@
         ) stmts
       #>> (split_list #> apsnd (map_filter I
         #> (fn [] => error ("Class block without class statement: "
-                  ^ (commas o map (labelled_name o fst)) stmts)
+                  ^ (Library.commas o map (labelled_name o fst)) stmts)
              | [stmt] => ML_Class stmt)));
     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
           add_fun stmt
@@ -849,7 +849,7 @@
       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
           add_funs stmts
       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
-          (commas o map (labelled_name o fst)) stmts);
+          (Library.commas o map (labelled_name o fst)) stmts);
     fun add_stmts' stmts nsp_nodes =
       let
         val names as (name :: names') = map fst stmts;
@@ -858,9 +858,9 @@
         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
           handle Empty =>
             error ("Different namespace prefixes for mutual dependencies:\n"
-              ^ commas (map labelled_name names)
+              ^ Library.commas (map labelled_name names)
               ^ "\n"
-              ^ commas module_names);
+              ^ Library.commas module_names);
         val module_name_path = Long_Name.explode module_name;
         fun add_dep name name' =
           let

--- a/src/Tools/Code/code_printer.ML	Thu Aug 26 12:20:34 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Aug 26 12:30:43 2010 +0200
@@ -19,6 +19,7 @@
   val concat: Pretty.T list -> Pretty.T
   val brackets: Pretty.T list -> Pretty.T
   val enclose: string -> string -> Pretty.T list -> Pretty.T
+  val commas: Pretty.T list -> Pretty.T list
   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
   val semicolon: Pretty.T list -> Pretty.T
@@ -112,6 +113,7 @@
 fun xs @| y = xs @ [y];
 val str = Print_Mode.setmp [] Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
+val commas = Print_Mode.setmp [] Pretty.commas;
 fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
 val brackets = enclose "(" ")" o Pretty.breaks;
 fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);

--- a/src/Tools/Code/code_scala.ML	Thu Aug 26 12:20:34 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 12:30:43 2010 +0200
@@ -441,7 +441,7 @@
     (* print nodes *)
     fun print_implicits [] = NONE
       | print_implicits implicits = (SOME o Pretty.block)
-          (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits));
+          (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits));
     fun print_module base implicits p = Pretty.chunks2
       ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
         @ [p, str ("} /* object " ^ base ^ " */")]);