diff -r 49b885736e8f -r 89f654951200 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Aug 26 12:30:43 2010 +0200 +++ b/src/Tools/Code/code_target.ML Thu Aug 26 13:50:58 2010 +0200 @@ -111,7 +111,7 @@ -> (string -> Code_Printer.activated_const_syntax option) -> ((Pretty.T -> string) * (Pretty.T -> unit)) -> Code_Thingol.program - -> string list (*selected statements*) + -> (string list * string list) (*selected statements*) -> serialization; datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, @@ -254,7 +254,7 @@ |>> map_filter I; fun invoke_serializer thy abortable serializer literals reserved abs_includes - module_alias class instance tyco const module width args naming program2 names1 = + module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) = let val (names_class, class') = activate_syntax (Code_Thingol.lookup_class naming) class; @@ -275,14 +275,14 @@ val _ = if null empty_funs then () else error ("No code equations for " ^ commas (map (Sign.extern_const thy) empty_funs)); in - serializer module args (Code_Thingol.labelled_name thy program2) reserved includes - (Symtab.lookup module_alias) (Symtab.lookup class') - (Symtab.lookup tyco') (Symtab.lookup const') + serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes + (if is_some module_name then K module_name else Symtab.lookup module_alias) + (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const') (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width) - program4 names1 + program4 (names1, presentation_names) end; -fun mount_serializer thy alt_serializer target some_width module args naming program names = +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination = let val ((targets, abortable), default_width) = Targets.get thy; fun collapse_hierarchy target = @@ -299,6 +299,9 @@ val (modify, data) = collapse_hierarchy target; val serializer = the_default (case the_description data of Fundamental seri => #serializer seri) alt_serializer; + val presentation_names = stmt_names_of_destination destination; + val module_name = if null presentation_names + then raw_module_name else SOME "Code"; val reserved = the_reserved data; fun select_include names_all (name, (content, cs)) = if null cs then SOME (name, content) @@ -308,13 +311,14 @@ then SOME (name, content) else NONE; fun includes names_all = map_filter (select_include names_all) ((Symtab.dest o the_includes) data); - val module_alias = the_module_alias data; + val module_alias = the_module_alias data val { class, instance, tyco, const } = the_name_syntax data; val literals = the_literals thy target; val width = the_default default_width some_width; in invoke_serializer thy abortable serializer literals reserved - includes module_alias class instance tyco const module width args naming (modify program) names + includes module_alias class instance tyco const module_name width args + naming (modify program) (names, presentation_names) destination end; in