# HG changeset patch
# User haftmann
# Date 1282823458 -7200
# Node ID 89f654951200e5e6a368cb9adaef77dd346e3e32
# Parent  49b885736e8fa844d93195be898eb049fe91a903
tuned serializer interface

diff -r 49b885736e8f -r 89f654951200 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Aug 26 12:30:43 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Aug 26 13:50:58 2010 +0200
@@ -261,9 +261,8 @@
           end;
   in print_stmt end;
 
-fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
+fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
   let
-    val module_alias = if is_some module_name then K module_name else raw_module_alias;
     val reserved = Name.make_context reserved;
     val mk_name_module = mk_name_module reserved module_prefix module_alias program;
     fun add_stmt (name, (stmt, deps)) =
@@ -314,15 +313,14 @@
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
-fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
-    raw_reserved includes raw_module_alias
-    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_haskell module_prefix module_name string_classes labelled_name
+    raw_reserved includes module_alias
+    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+    (stmt_names, presentation_stmt_names) destination =
   let
-    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
-    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
-      module_name module_prefix reserved raw_module_alias program;
+      module_prefix reserved module_alias program;
     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
     fun deriving_show tyco =
       let
diff -r 49b885736e8f -r 89f654951200 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Aug 26 12:30:43 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 13:50:58 2010 +0200
@@ -722,9 +722,8 @@
 
 in
 
-fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
+fun ml_node_of_program labelled_name module_name reserved module_alias program =
   let
-    val module_alias = if is_some module_name then K module_name else raw_module_alias;
     val reserved = Name.make_context reserved;
     val empty_module = ((reserved, reserved), Graph.empty);
     fun map_node [] f = f
@@ -907,15 +906,14 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
-  reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
+  reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+  (stmt_names, presentation_stmt_names) =
   let
     val is_cons = Code_Thingol.is_cons program;
-    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
     val is_presentation = not (null presentation_stmt_names);
-    val module_name = if is_presentation then SOME "Code" else raw_module_name;
     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
-      reserved raw_module_alias program;
+      reserved module_alias program;
     val reserved = make_vars reserved;
     fun print_node prefix (Dummy _) =
           NONE
@@ -939,7 +937,7 @@
   in
     Code_Target.mk_serialization target
       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
-      (rpair stmt_names' o code_of_pretty) p destination
+      (rpair stmt_names' o code_of_pretty) p
   end;
 
 end; (*local*)
diff -r 49b885736e8f -r 89f654951200 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Aug 26 12:30:43 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 13:50:58 2010 +0200
@@ -293,11 +293,10 @@
 
 in
 
-fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
+fun scala_program_of_program labelled_name reserved module_alias program =
   let
 
     (* building module name hierarchy *)
-    val module_alias = if is_some module_name then K module_name else raw_module_alias;
     fun alias_fragments name = case module_alias name
      of SOME name' => Long_Name.explode name'
       | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
@@ -403,20 +402,15 @@
 
   in (deresolve, sca_program) end;
 
-fun serialize_scala raw_module_name labelled_name
-    raw_reserved includes raw_module_alias
+fun serialize_scala labelled_name raw_reserved includes module_alias
     _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
-    program stmt_names destination =
+    program (stmt_names, presentation_stmt_names) destination =
   let
 
-    (* generic nonsense *)
-    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
-    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
-
     (* preprocess program *)
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolve, sca_program) = scala_program_of_program labelled_name
-      module_name (Name.make_context reserved) raw_module_alias program;
+      (Name.make_context reserved) module_alias program;
 
     (* print statements *)
     fun lookup_constr tyco constr = case Graph.get_node program tyco
@@ -498,9 +492,9 @@
 
 (** Isar setup **)
 
-fun isar_serializer module_name =
+fun isar_serializer _ =
   Code_Target.parse_args (Scan.succeed ())
-  #> (fn () => serialize_scala module_name);
+  #> (fn () => serialize_scala);
 
 val setup =
   Code_Target.add_target
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