1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 14:36:49 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 14:59:28 2010 +0200
     1.3 @@ -334,7 +334,7 @@
     1.4  fun serialize_haskell module_prefix string_classes { labelled_name,
     1.5      reserved_syms, includes, module_alias,
     1.6      class_syntax, tyco_syntax, const_syntax, program,
     1.7 -    names, presentation_names } =
     1.8 +    names } =
     1.9    let
    1.10      val reserved = fold (insert (op =) o fst) includes reserved_syms;
    1.11      val (deresolver, hs_program) = haskell_program_of_program labelled_name

     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 14:36:49 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 14:59:28 2010 +0200
     2.3 @@ -787,7 +787,7 @@
     2.4  
     2.5  fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
     2.6    reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
     2.7 -  const_syntax, program, names, presentation_names } =
     2.8 +  const_syntax, program, names } =
     2.9    let
    2.10      val is_cons = Code_Thingol.is_cons program;
    2.11      val { deresolver, hierarchical_program = ml_program } =

     3.1 --- a/src/Tools/Code/code_scala.ML	Thu Sep 02 14:36:49 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 14:59:28 2010 +0200
     3.3 @@ -329,7 +329,7 @@
     3.4  
     3.5  fun serialize_scala { labelled_name, reserved_syms, includes,
     3.6      module_alias, class_syntax, tyco_syntax, const_syntax, program,
     3.7 -    names, presentation_names } =
     3.8 +    names } =
     3.9    let
    3.10  
    3.11      (* build program *)

     4.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 14:36:49 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 14:59:28 2010 +0200
     4.3 @@ -73,9 +73,6 @@
     4.4  datatype destination = Export of Path.T option | Produce | Present of string list;
     4.5  type serialization = int -> destination -> (string * string option list) option;
     4.6  
     4.7 -fun stmt_names_of_destination (Present stmt_names) = stmt_names
     4.8 -  | stmt_names_of_destination _ = [];
     4.9 -
    4.10  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    4.11    | serialization _ string content width Produce = SOME (string [] width content)
    4.12    | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
    4.13 @@ -117,8 +114,7 @@
    4.14      tyco_syntax: string -> Code_Printer.tyco_syntax option,
    4.15      const_syntax: string -> Code_Printer.activated_const_syntax option,
    4.16      program: Code_Thingol.program,
    4.17 -    names: string list,
    4.18 -    presentation_names: string list }
    4.19 +    names: string list }
    4.20    -> serialization;
    4.21  
    4.22  datatype description = Fundamental of { serializer: serializer,
    4.23 @@ -309,7 +305,7 @@
    4.24  
    4.25  fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    4.26      module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
    4.27 -    module_name args naming proto_program (names, presentation_names) =
    4.28 +    module_name args naming proto_program names =
    4.29    let
    4.30      val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
    4.31        activate_symbol_syntax thy literals naming
    4.32 @@ -326,19 +322,15 @@
    4.33        tyco_syntax = Symtab.lookup tyco_syntax,
    4.34        const_syntax = Symtab.lookup const_syntax,
    4.35        program = program,
    4.36 -      names = names,
    4.37 -      presentation_names = presentation_names }
    4.38 +      names = names }
    4.39    end;
    4.40  
    4.41 -fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination =
    4.42 +fun mount_serializer thy target some_width module_name args naming proto_program names =
    4.43    let
    4.44      val (default_width, abortable, data, program) =
    4.45        activate_target_for thy target naming proto_program;
    4.46      val serializer = case the_description data
    4.47       of Fundamental seri => #serializer seri;
    4.48 -    val presentation_names = stmt_names_of_destination destination;
    4.49 -    val module_name = if null presentation_names
    4.50 -      then raw_module_name else "Code";
    4.51      val reserved = the_reserved data;
    4.52      fun select_include names_all (name, (content, cs)) =
    4.53        if null cs then SOME (name, content)
    4.54 @@ -355,7 +347,7 @@
    4.55    in
    4.56      invoke_serializer thy abortable serializer literals reserved
    4.57        includes module_alias class instance tyco const module_name args
    4.58 -        naming program (names, presentation_names) width destination
    4.59 +        naming program names width
    4.60    end;
    4.61  
    4.62  fun assert_module_name "" = error ("Empty module name not allowed.")