1.1 --- a/src/Tools/Code/code_target.ML	Thu Aug 26 12:30:43 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Aug 26 13:50:58 2010 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    -> (string -> Code_Printer.activated_const_syntax option)
     1.5    -> ((Pretty.T -> string) * (Pretty.T -> unit))
     1.6    -> Code_Thingol.program
     1.7 -  -> string list                        (*selected statements*)
     1.8 +  -> (string list * string list)        (*selected statements*)
     1.9    -> serialization;
    1.10  
    1.11  datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
    1.12 @@ -254,7 +254,7 @@
    1.13    |>> map_filter I;
    1.14  
    1.15  fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    1.16 -    module_alias class instance tyco const module width args naming program2 names1 =
    1.17 +    module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
    1.18    let
    1.19      val (names_class, class') =
    1.20        activate_syntax (Code_Thingol.lookup_class naming) class;
    1.21 @@ -275,14 +275,14 @@
    1.22      val _ = if null empty_funs then () else error ("No code equations for "
    1.23        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.24    in
    1.25 -    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    1.26 -      (Symtab.lookup module_alias) (Symtab.lookup class')
    1.27 -      (Symtab.lookup tyco') (Symtab.lookup const')
    1.28 +    serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
    1.29 +      (if is_some module_name then K module_name else Symtab.lookup module_alias)
    1.30 +      (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    1.31        (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    1.32 -      program4 names1
    1.33 +      program4 (names1, presentation_names)
    1.34    end;
    1.35  
    1.36 -fun mount_serializer thy alt_serializer target some_width module args naming program names =
    1.37 +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
    1.38    let
    1.39      val ((targets, abortable), default_width) = Targets.get thy;
    1.40      fun collapse_hierarchy target =
    1.41 @@ -299,6 +299,9 @@
    1.42      val (modify, data) = collapse_hierarchy target;
    1.43      val serializer = the_default (case the_description data
    1.44       of Fundamental seri => #serializer seri) alt_serializer;
    1.45 +    val presentation_names = stmt_names_of_destination destination;
    1.46 +    val module_name = if null presentation_names
    1.47 +      then raw_module_name else SOME "Code";
    1.48      val reserved = the_reserved data;
    1.49      fun select_include names_all (name, (content, cs)) =
    1.50        if null cs then SOME (name, content)
    1.51 @@ -308,13 +311,14 @@
    1.52        then SOME (name, content) else NONE;
    1.53      fun includes names_all = map_filter (select_include names_all)
    1.54        ((Symtab.dest o the_includes) data);
    1.55 -    val module_alias = the_module_alias data;
    1.56 +    val module_alias = the_module_alias data 
    1.57      val { class, instance, tyco, const } = the_name_syntax data;
    1.58      val literals = the_literals thy target;
    1.59      val width = the_default default_width some_width;
    1.60    in
    1.61      invoke_serializer thy abortable serializer literals reserved
    1.62 -      includes module_alias class instance tyco const module width args naming (modify program) names
    1.63 +      includes module_alias class instance tyco const module_name width args
    1.64 +        naming (modify program) (names, presentation_names) destination
    1.65    end;
    1.66  
    1.67  in