# HG changeset patch
# User haftmann
# Date 1283432368 -7200
# Node ID 551fe1af03b00545e7e21b3c95791564ac4cc608
# Parent  c6d146ed07aedb35a45c6c371a2f89e32f698e5a
dropped superfluous presentation names

diff -r c6d146ed07ae -r 551fe1af03b0 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 14:36:49 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 14:59:28 2010 +0200
@@ -334,7 +334,7 @@
 fun serialize_haskell module_prefix string_classes { labelled_name,
     reserved_syms, includes, module_alias,
     class_syntax, tyco_syntax, const_syntax, program,
-    names, presentation_names } =
+    names } =
   let
     val reserved = fold (insert (op =) o fst) includes reserved_syms;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
diff -r c6d146ed07ae -r 551fe1af03b0 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 14:36:49 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 14:59:28 2010 +0200
@@ -787,7 +787,7 @@
 
 fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
   reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
-  const_syntax, program, names, presentation_names } =
+  const_syntax, program, names } =
   let
     val is_cons = Code_Thingol.is_cons program;
     val { deresolver, hierarchical_program = ml_program } =
diff -r c6d146ed07ae -r 551fe1af03b0 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Sep 02 14:36:49 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 14:59:28 2010 +0200
@@ -329,7 +329,7 @@
 
 fun serialize_scala { labelled_name, reserved_syms, includes,
     module_alias, class_syntax, tyco_syntax, const_syntax, program,
-    names, presentation_names } =
+    names } =
   let
 
     (* build program *)
diff -r c6d146ed07ae -r 551fe1af03b0 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Sep 02 14:36:49 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 02 14:59:28 2010 +0200
@@ -73,9 +73,6 @@
 datatype destination = Export of Path.T option | Produce | Present of string list;
 type serialization = int -> destination -> (string * string option list) option;
 
-fun stmt_names_of_destination (Present stmt_names) = stmt_names
-  | stmt_names_of_destination _ = [];
-
 fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
   | serialization _ string content width Produce = SOME (string [] width content)
   | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
@@ -117,8 +114,7 @@
     tyco_syntax: string -> Code_Printer.tyco_syntax option,
     const_syntax: string -> Code_Printer.activated_const_syntax option,
     program: Code_Thingol.program,
-    names: string list,
-    presentation_names: string list }
+    names: string list }
   -> serialization;
 
 datatype description = Fundamental of { serializer: serializer,
@@ -309,7 +305,7 @@
 
 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
-    module_name args naming proto_program (names, presentation_names) =
+    module_name args naming proto_program names =
   let
     val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
       activate_symbol_syntax thy literals naming
@@ -326,19 +322,15 @@
       tyco_syntax = Symtab.lookup tyco_syntax,
       const_syntax = Symtab.lookup const_syntax,
       program = program,
-      names = names,
-      presentation_names = presentation_names }
+      names = names }
   end;
 
-fun mount_serializer thy target some_width raw_module_name args naming proto_program names destination =
+fun mount_serializer thy target some_width module_name args naming proto_program names =
   let
     val (default_width, abortable, data, program) =
       activate_target_for thy target naming proto_program;
     val serializer = case the_description data
      of Fundamental seri => #serializer seri;
-    val presentation_names = stmt_names_of_destination destination;
-    val module_name = if null presentation_names
-      then raw_module_name else "Code";
     val reserved = the_reserved data;
     fun select_include names_all (name, (content, cs)) =
       if null cs then SOME (name, content)
@@ -355,7 +347,7 @@
   in
     invoke_serializer thy abortable serializer literals reserved
       includes module_alias class instance tyco const module_name args
-        naming program (names, presentation_names) width destination
+        naming program names width
   end;
 
 fun assert_module_name "" = error ("Empty module name not allowed.")