1.1 --- a/src/Tools/Code/code_ml.ML	Thu Aug 26 12:20:34 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 12:30:43 2010 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
     1.5                        (insert (op =)) ts []);
     1.6                in concat [
     1.7 -                (Pretty.block o Pretty.commas)
     1.8 +                (Pretty.block o commas)
     1.9                    (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
    1.10                  str "->",
    1.11                  print_term is_pseudo_fun some_thm vars NOBR t
    1.12 @@ -535,7 +535,7 @@
    1.13                        :: Pretty.brk 1
    1.14                        :: str "match"
    1.15                        :: Pretty.brk 1
    1.16 -                      :: (Pretty.block o Pretty.commas) dummy_parms
    1.17 +                      :: (Pretty.block o commas) dummy_parms
    1.18                        :: Pretty.brk 1
    1.19                        :: str "with"
    1.20                        :: Pretty.brk 1
    1.21 @@ -813,7 +813,7 @@
    1.22          ) stmts
    1.23        #>> (split_list #> apsnd (map_filter I
    1.24          #> (fn [] => error ("Datatype block without data statement: "
    1.25 -                  ^ (commas o map (labelled_name o fst)) stmts)
    1.26 +                  ^ (Library.commas o map (labelled_name o fst)) stmts)
    1.27               | stmts => ML_Datas stmts)));
    1.28      fun add_class stmts =
    1.29        fold_map
    1.30 @@ -828,7 +828,7 @@
    1.31          ) stmts
    1.32        #>> (split_list #> apsnd (map_filter I
    1.33          #> (fn [] => error ("Class block without class statement: "
    1.34 -                  ^ (commas o map (labelled_name o fst)) stmts)
    1.35 +                  ^ (Library.commas o map (labelled_name o fst)) stmts)
    1.36               | [stmt] => ML_Class stmt)));
    1.37      fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
    1.38            add_fun stmt
    1.39 @@ -849,7 +849,7 @@
    1.40        | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
    1.41            add_funs stmts
    1.42        | add_stmts stmts = error ("Illegal mutual dependencies: " ^
    1.43 -          (commas o map (labelled_name o fst)) stmts);
    1.44 +          (Library.commas o map (labelled_name o fst)) stmts);
    1.45      fun add_stmts' stmts nsp_nodes =
    1.46        let
    1.47          val names as (name :: names') = map fst stmts;
    1.48 @@ -858,9 +858,9 @@
    1.49          val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
    1.50            handle Empty =>
    1.51              error ("Different namespace prefixes for mutual dependencies:\n"
    1.52 -              ^ commas (map labelled_name names)
    1.53 +              ^ Library.commas (map labelled_name names)
    1.54                ^ "\n"
    1.55 -              ^ commas module_names);
    1.56 +              ^ Library.commas module_names);
    1.57          val module_name_path = Long_Name.explode module_name;
    1.58          fun add_dep name name' =
    1.59            let

     2.1 --- a/src/Tools/Code/code_printer.ML	Thu Aug 26 12:20:34 2010 +0200
     2.2 +++ b/src/Tools/Code/code_printer.ML	Thu Aug 26 12:30:43 2010 +0200
     2.3 @@ -19,6 +19,7 @@
     2.4    val concat: Pretty.T list -> Pretty.T
     2.5    val brackets: Pretty.T list -> Pretty.T
     2.6    val enclose: string -> string -> Pretty.T list -> Pretty.T
     2.7 +  val commas: Pretty.T list -> Pretty.T list
     2.8    val enum: string -> string -> string -> Pretty.T list -> Pretty.T
     2.9    val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    2.10    val semicolon: Pretty.T list -> Pretty.T
    2.11 @@ -112,6 +113,7 @@
    2.12  fun xs @| y = xs @ [y];
    2.13  val str = Print_Mode.setmp [] Pretty.str;
    2.14  val concat = Pretty.block o Pretty.breaks;
    2.15 +val commas = Print_Mode.setmp [] Pretty.commas;
    2.16  fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
    2.17  val brackets = enclose "(" ")" o Pretty.breaks;
    2.18  fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);

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