1.1 --- a/src/Tools/Code/code_haskell.ML	Tue Aug 31 14:06:20 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Aug 31 14:21:06 2010 +0200
     1.3 @@ -313,12 +313,12 @@
     1.4        handle Option => error ("Unknown statement name: " ^ labelled_name name);
     1.5    in (deresolver, hs_program) end;
     1.6  
     1.7 -fun serialize_haskell module_prefix string_classes labelled_name
     1.8 -    raw_reserved includes single_module module_alias
     1.9 -    class_syntax tyco_syntax const_syntax program
    1.10 -    (stmt_names, presentation_stmt_names) =
    1.11 +fun serialize_haskell module_prefix string_classes { labelled_name,
    1.12 +    reserved_syms, includes, single_module, module_alias,
    1.13 +    class_syntax, tyco_syntax, const_syntax, program,
    1.14 +    names, presentation_names } =
    1.15    let
    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, hs_program) = haskell_program_of_program labelled_name
    1.19        module_prefix reserved module_alias program;
    1.20      val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
    1.21 @@ -368,13 +368,13 @@
    1.22            );
    1.23        in print_module module_name' content end;
    1.24      fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
    1.25 -        (fn (name, (_, SOME stmt)) => if null presentation_stmt_names
    1.26 -              orelse member (op =) presentation_stmt_names name
    1.27 +        (fn (name, (_, SOME stmt)) => if null presentation_names
    1.28 +              orelse member (op =) presentation_names name
    1.29                then SOME (print_stmt false (name, stmt))
    1.30                else NONE
    1.31            | (_, (_, NONE)) => NONE) stmts);
    1.32      val serialize_module =
    1.33 -      if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2;
    1.34 +      if null presentation_names then serialize_module1 else pair "" o serialize_module2;
    1.35      fun write_module width (SOME destination) (modlname, content) =
    1.36            let
    1.37              val _ = File.check destination;

     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Aug 31 14:06:20 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 14:21:06 2010 +0200
     2.3 @@ -902,19 +902,19 @@
     2.4          error ("Unknown statement name: " ^ labelled_name name);
     2.5    in (deresolver, nodes) end;
     2.6  
     2.7 -fun serialize_ml target print_module print_stmt with_signatures labelled_name
     2.8 -  reserved includes single_module module_alias _ tyco_syntax const_syntax program
     2.9 -  (stmt_names, presentation_stmt_names) =
    2.10 +fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
    2.11 +  reserved_syms, includes, single_module, module_alias, class_syntax, tyco_syntax,
    2.12 +  const_syntax, program, names, presentation_names } =
    2.13    let
    2.14      val is_cons = Code_Thingol.is_cons program;
    2.15 -    val is_presentation = not (null presentation_stmt_names);
    2.16 +    val is_presentation = not (null presentation_names);
    2.17      val (deresolver, nodes) = ml_node_of_program labelled_name
    2.18 -      reserved module_alias program;
    2.19 -    val reserved = make_vars reserved;
    2.20 +      reserved_syms module_alias program;
    2.21 +    val reserved = make_vars reserved_syms;
    2.22      fun print_node prefix (Dummy _) =
    2.23            NONE
    2.24        | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
    2.25 -          (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
    2.26 +          (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
    2.27            then NONE
    2.28            else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
    2.29        | print_node prefix (Module (module_name, (_, nodes))) =
    2.30 @@ -927,13 +927,13 @@
    2.31          o rev o flat o Graph.strong_conn) nodes
    2.32        |> split_list
    2.33        |> (fn (decls, body) => (flat decls, body))
    2.34 -    val stmt_names' = map (try (deresolver [])) stmt_names
    2.35 +    val names' = map (try (deresolver [])) names
    2.36        |> single_module ? (map o Option.map) Long_Name.base_name;
    2.37      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
    2.38      fun write width NONE = writeln_pretty width
    2.39        | write width (SOME p) = File.write p o string_of_pretty width;
    2.40    in
    2.41 -    Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
    2.42 +    Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
    2.43    end;
    2.44  
    2.45  end; (*local*)

     3.1 --- a/src/Tools/Code/code_scala.ML	Tue Aug 31 14:06:20 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 14:21:06 2010 +0200
     3.3 @@ -413,13 +413,13 @@
     3.4  
     3.5    in (deresolver, sca_program) end;
     3.6  
     3.7 -fun serialize_scala labelled_name raw_reserved includes _ module_alias
     3.8 -    _ tyco_syntax const_syntax
     3.9 -    program (stmt_names, presentation_stmt_names) =
    3.10 +fun serialize_scala { labelled_name, reserved_syms, includes, single_module,
    3.11 +    module_alias, class_syntax, tyco_syntax, const_syntax, program,
    3.12 +    names, presentation_names } =
    3.13    let
    3.14  
    3.15      (* build program *)
    3.16 -    val reserved = fold (insert (op =) o fst) includes raw_reserved;
    3.17 +    val reserved = fold (insert (op =) o fst) includes reserved_syms;
    3.18      val (deresolver, sca_program) = scala_program_of_program labelled_name
    3.19        (Name.make_context reserved) module_alias program;
    3.20  
    3.21 @@ -455,12 +455,12 @@
    3.22        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
    3.23      fun print_node _ (_, Dummy) = NONE
    3.24        | print_node prefix_fragments (name, Stmt stmt) =
    3.25 -          if null presentation_stmt_names
    3.26 -          orelse member (op =) presentation_stmt_names name
    3.27 +          if null presentation_names
    3.28 +          orelse member (op =) presentation_names name
    3.29            then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
    3.30            else NONE
    3.31        | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
    3.32 -          if null presentation_stmt_names
    3.33 +          if null presentation_names
    3.34            then
    3.35              let
    3.36                val prefix_fragments' = prefix_fragments @ [name_fragment];
    3.37 @@ -477,7 +477,7 @@
    3.38        in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
    3.39  
    3.40      (* serialization *)
    3.41 -    val p_includes = if null presentation_stmt_names
    3.42 +    val p_includes = if null presentation_names
    3.43        then map (fn (base, p) => print_module base [] p) includes else [];
    3.44      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    3.45      fun write width NONE = writeln_pretty width

     4.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 14:06:20 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 14:21:06 2010 +0200
     4.3 @@ -101,17 +101,18 @@
     4.4         Symtab.join (K snd) (const1, const2))
     4.5    );
     4.6  
     4.7 -type serializer = Token.T list          (*arguments*)
     4.8 -  -> (string -> string)                 (*labelled_name*)
     4.9 -  -> string list                        (*reserved symbols*)
    4.10 -  -> (string * Pretty.T) list           (*includes*)
    4.11 -  -> bool                               (*singleton module*)
    4.12 -  -> (string -> string option)          (*module aliasses*)
    4.13 -  -> (string -> string option)          (*class syntax*)
    4.14 -  -> (string -> Code_Printer.tyco_syntax option)
    4.15 -  -> (string -> Code_Printer.activated_const_syntax option)
    4.16 -  -> Code_Thingol.program
    4.17 -  -> (string list * string list)        (*selected statements*)
    4.18 +type serializer = Token.T list (*arguments*) -> {
    4.19 +    labelled_name: string -> string,
    4.20 +    reserved_syms: string list,
    4.21 +    includes: (string * Pretty.T) list,
    4.22 +    single_module: bool,
    4.23 +    module_alias: string -> string option,
    4.24 +    class_syntax: string -> string option,
    4.25 +    tyco_syntax: string -> Code_Printer.tyco_syntax option,
    4.26 +    const_syntax: string -> Code_Printer.activated_const_syntax option,
    4.27 +    program: Code_Thingol.program,
    4.28 +    names: string list,
    4.29 +    presentation_names: string list }
    4.30    -> serialization;
    4.31  
    4.32  datatype description = Fundamental of { serializer: serializer,
    4.33 @@ -277,10 +278,18 @@
    4.34      val _ = if null empty_funs then () else error ("No code equations for "
    4.35        ^ commas (map (Sign.extern_const thy) empty_funs));
    4.36    in
    4.37 -    serializer args (Code_Thingol.labelled_name thy program2) reserved includes
    4.38 -      (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias)
    4.39 -      (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    4.40 -      program4 (names1, presentation_names) width
    4.41 +    serializer args {
    4.42 +      labelled_name = Code_Thingol.labelled_name thy program2,
    4.43 +      reserved_syms = reserved,
    4.44 +      includes = includes,
    4.45 +      single_module = is_some module_name,
    4.46 +      module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
    4.47 +      class_syntax = Symtab.lookup class',
    4.48 +      tyco_syntax = Symtab.lookup tyco',
    4.49 +      const_syntax = Symtab.lookup const',
    4.50 +      program = program3,
    4.51 +      names = names1,
    4.52 +      presentation_names = presentation_names } width
    4.53    end;
    4.54  
    4.55  fun mount_serializer thy target some_width raw_module_name args naming program names destination =