improved deresolving of implicits
authorhaftmann
Fri Aug 27 15:36:02 2010 +0200 (2010-08-27)
changeset 38856168dba35ecf3
parent 38815 d0196406ee32
child 38857 97775f3e8722
improved deresolving of implicits
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_scala.ML	Fri Aug 27 14:25:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Fri Aug 27 15:36:02 2010 +0200
     1.3 @@ -444,18 +444,15 @@
     1.4        (make_vars reserved) args_num is_singleton_constr;
     1.5  
     1.6      (* print nodes *)
     1.7 +    fun print_module base implicit_ps p = Pretty.chunks2
     1.8 +      ([str ("object " ^ base ^ " {")]
     1.9 +        @ (if null implicit_ps then [] else (single o Pretty.block)
    1.10 +            (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
    1.11 +        @ [p, str ("} /* object " ^ base ^ " */")]);
    1.12      fun print_implicit prefix_fragments implicit =
    1.13        let
    1.14          val s = deresolver prefix_fragments implicit;
    1.15        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
    1.16 -    fun print_implicits prefix_fragments implicits =
    1.17 -      case map_filter (print_implicit prefix_fragments) implicits
    1.18 -       of [] => NONE
    1.19 -        | ps => (SOME o Pretty.block)
    1.20 -            (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
    1.21 -    fun print_module prefix_fragments base implicits p = Pretty.chunks2
    1.22 -      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
    1.23 -        @ [p, str ("} /* object " ^ base ^ " */")]);
    1.24      fun print_node _ (_, Dummy) = NONE
    1.25        | print_node prefix_fragments (name, Stmt stmt) =
    1.26            if null presentation_stmt_names
    1.27 @@ -464,10 +461,14 @@
    1.28            else NONE
    1.29        | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
    1.30            if null presentation_stmt_names
    1.31 -          then case print_nodes (prefix_fragments @ [name_fragment]) nodes
    1.32 -           of NONE => NONE
    1.33 -            | SOME p => SOME (print_module prefix_fragments
    1.34 -                (Long_Name.base_name name_fragment) implicits p)
    1.35 +          then
    1.36 +            let
    1.37 +              val prefix_fragments' = prefix_fragments @ [name_fragment];
    1.38 +            in
    1.39 +              Option.map (print_module name_fragment
    1.40 +                (map_filter (print_implicit prefix_fragments') implicits))
    1.41 +                  (print_nodes prefix_fragments' nodes)
    1.42 +            end
    1.43            else print_nodes [] nodes
    1.44      and print_nodes prefix_fragments nodes = let
    1.45          val ps = map_filter (fn name => print_node prefix_fragments (name,
    1.46 @@ -477,7 +478,7 @@
    1.47  
    1.48      (* serialization *)
    1.49      val p_includes = if null presentation_stmt_names
    1.50 -      then map (fn (base, p) => print_module [] base [] p) includes else [];
    1.51 +      then map (fn (base, p) => print_module base [] p) includes else [];
    1.52      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    1.53    in
    1.54      Code_Target.mk_serialization target