src/Tools/Code/code_target.ML

   -> (string -> string option)          (*class syntax*)
   -> (string -> Code_Printer.tyco_syntax option)
   -> (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,
       check: { env_var: string, make_destination: Path.T -> Path.T,
         make_command: string -> Path.T -> string -> string } }

             in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
         | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
   |>> 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;
     val names_inst = map_filter (Code_Thingol.lookup_instance naming)
       (Symreltab.keys instance);

     val empty_funs = filter_out (member (op =) abortable)
       (Code_Thingol.empty_funs program3);
     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 =
       let
         val data = case Symtab.lookup targets target

           in (modify' #> modify naming, merge_target false target (data', data)) end
       end;
     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)
       else if exists (fn c => case Code_Thingol.lookup_const naming c
        of SOME name => member (op =) names_all name
         | NONE => false) cs
       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
 
 fun serialize thy = mount_serializer thy NONE;