1.1 --- a/src/Tools/Code/code_scala.ML	Tue Aug 31 14:06:20 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 14:21:06 2010 +0200
     1.3 @@ -413,13 +413,13 @@
     1.4  
     1.5    in (deresolver, sca_program) end;
     1.6  
     1.7 -fun serialize_scala labelled_name raw_reserved includes _ module_alias
     1.8 -    _ tyco_syntax const_syntax
     1.9 -    program (stmt_names, presentation_stmt_names) =
    1.10 +fun serialize_scala { labelled_name, reserved_syms, includes, single_module,
    1.11 +    module_alias, class_syntax, tyco_syntax, const_syntax, program,
    1.12 +    names, presentation_names } =
    1.13    let
    1.14  
    1.15      (* build program *)
    1.16 -    val reserved = fold (insert (op =) o fst) includes raw_reserved;
    1.17 +    val reserved = fold (insert (op =) o fst) includes reserved_syms;
    1.18      val (deresolver, sca_program) = scala_program_of_program labelled_name
    1.19        (Name.make_context reserved) module_alias program;
    1.20  
    1.21 @@ -455,12 +455,12 @@
    1.22        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
    1.23      fun print_node _ (_, Dummy) = NONE
    1.24        | print_node prefix_fragments (name, Stmt stmt) =
    1.25 -          if null presentation_stmt_names
    1.26 -          orelse member (op =) presentation_stmt_names name
    1.27 +          if null presentation_names
    1.28 +          orelse member (op =) presentation_names name
    1.29            then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
    1.30            else NONE
    1.31        | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
    1.32 -          if null presentation_stmt_names
    1.33 +          if null presentation_names
    1.34            then
    1.35              let
    1.36                val prefix_fragments' = prefix_fragments @ [name_fragment];
    1.37 @@ -477,7 +477,7 @@
    1.38        in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
    1.39  
    1.40      (* serialization *)
    1.41 -    val p_includes = if null presentation_stmt_names
    1.42 +    val p_includes = if null presentation_names
    1.43        then map (fn (base, p) => print_module base [] p) includes else [];
    1.44      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    1.45      fun write width NONE = writeln_pretty width