# HG changeset patch
# User haftmann
# Date 1282824253 -7200
# Node ID 3865cbe5d2be2456ee579a40ce6fd7c393091c62
# Parent  6b356e3687d25e1a8252120107df4556f95fd508
only print qualified implicits

diff -r 6b356e3687d2 -r 3865cbe5d2be src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Aug 26 13:56:35 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 14:04:13 2010 +0200
@@ -434,9 +434,14 @@
       (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
 
     (* print nodes *)
-    fun print_implicits [] = NONE
-      | print_implicits implicits = (SOME o Pretty.block)
-          (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits));
+    fun print_implicit implicit =
+      let
+        val s = deresolve implicit;
+      in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
+    fun print_implicits implicits = case map_filter print_implicit implicits
+     of [] => NONE
+      | ps => (SOME o Pretty.block)
+          (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
     fun print_module base implicits p = Pretty.chunks2
       ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
         @ [p, str ("} /* object " ^ base ^ " */")]);