--- 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.")