1.1 --- a/src/Tools/Code/code_scala.ML	Thu Aug 26 13:56:35 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 14:04:13 2010 +0200
     1.3 @@ -434,9 +434,14 @@
     1.4        (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
     1.5  
     1.6      (* print nodes *)
     1.7 -    fun print_implicits [] = NONE
     1.8 -      | print_implicits implicits = (SOME o Pretty.block)
     1.9 -          (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits));
    1.10 +    fun print_implicit implicit =
    1.11 +      let
    1.12 +        val s = deresolve implicit;
    1.13 +      in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
    1.14 +    fun print_implicits implicits = case map_filter print_implicit implicits
    1.15 +     of [] => NONE
    1.16 +      | ps => (SOME o Pretty.block)
    1.17 +          (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
    1.18      fun print_module base implicits p = Pretty.chunks2
    1.19        ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
    1.20          @ [p, str ("} /* object " ^ base ^ " */")]);