# HG changeset patch
# User haftmann
# Date 1283255754 -7200
# Node ID fcd1d0457e27e9651b28e4a490c663d9c1e677b8
# Parent  79d7f2b4cf713ca8321845f65987f3101d293488
removed serializer interface redundancies

diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:29:38 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:55:54 2010 +0200
@@ -313,8 +313,8 @@
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
-fun serialize_haskell module_prefix module_name string_classes labelled_name
-    raw_reserved includes module_alias
+fun serialize_haskell module_prefix string_classes labelled_name
+    raw_reserved includes single_module module_alias
     class_syntax tyco_syntax const_syntax program
     (stmt_names, presentation_stmt_names) =
   let
@@ -350,7 +350,7 @@
     fun serialize_module1 (module_name', (deps, (stmts, _))) =
       let
         val stmt_names = map fst stmts;
-        val qualified = is_none module_name;
+        val qualified = not single_module;
         val imports = subtract (op =) stmt_names deps
           |> distinct (op =)
           |> map_filter (try deresolver)
@@ -465,11 +465,11 @@
 
 (** Isar setup **)
 
-fun isar_serializer module_name =
+val isar_serializer =
   Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
     >> (fn (module_prefix, string_classes) =>
-      serialize_haskell module_prefix module_name string_classes));
+      serialize_haskell module_prefix string_classes));
 
 val _ =
   Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Aug 31 13:29:38 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:55:54 2010 +0200
@@ -718,7 +718,7 @@
 
 in
 
-fun ml_node_of_program labelled_name module_name reserved module_alias program =
+fun ml_node_of_program labelled_name reserved module_alias program =
   let
     val reserved = Name.make_context reserved;
     val empty_module = ((reserved, reserved), Graph.empty);
@@ -902,13 +902,13 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
-  reserved includes module_alias _ tyco_syntax const_syntax program
+fun serialize_ml target print_module print_stmt with_signatures labelled_name
+  reserved includes single_module module_alias _ tyco_syntax const_syntax program
   (stmt_names, presentation_stmt_names) =
   let
     val is_cons = Code_Thingol.is_cons program;
     val is_presentation = not (null presentation_stmt_names);
-    val (deresolver, nodes) = ml_node_of_program labelled_name module_name
+    val (deresolver, nodes) = ml_node_of_program labelled_name
       reserved module_alias program;
     val reserved = make_vars reserved;
     fun print_node prefix (Dummy _) =
@@ -927,8 +927,8 @@
         o rev o flat o Graph.strong_conn) nodes
       |> split_list
       |> (fn (decls, body) => (flat decls, body))
-    val stmt_names' = (map o try)
-      (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
+    val stmt_names' = map (try (deresolver [])) stmt_names
+      |> single_module ? (map o Option.map) Long_Name.base_name;
     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
     fun write width NONE = writeln_pretty width
       | write width (SOME p) = File.write p o string_of_pretty width;
@@ -941,15 +941,15 @@
 
 (** Isar setup **)
 
-fun isar_serializer_sml module_name =
+val isar_serializer_sml =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   >> (fn with_signatures => serialize_ml target_SML
-      print_sml_module print_sml_stmt module_name with_signatures));
+      print_sml_module print_sml_stmt with_signatures));
 
-fun isar_serializer_ocaml module_name =
+val isar_serializer_ocaml =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   >> (fn with_signatures => serialize_ml target_OCaml
-      print_ocaml_module print_ocaml_stmt module_name with_signatures));
+      print_ocaml_module print_ocaml_stmt with_signatures));
 
 val setup =
   Code_Target.add_target
diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Aug 31 13:29:38 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 13:55:54 2010 +0200
@@ -413,7 +413,7 @@
 
   in (deresolver, sca_program) end;
 
-fun serialize_scala labelled_name raw_reserved includes module_alias
+fun serialize_scala labelled_name raw_reserved includes _ module_alias
     _ tyco_syntax const_syntax
     program (stmt_names, presentation_stmt_names) =
   let
@@ -513,9 +513,8 @@
 
 (** Isar setup **)
 
-fun isar_serializer _ =
-  Code_Target.parse_args (Scan.succeed ())
-  #> (fn () => serialize_scala);
+val isar_serializer =
+  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
 
 val setup =
   Code_Target.add_target
diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Aug 31 13:29:38 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:55:54 2010 +0200
@@ -101,12 +101,11 @@
        Symtab.join (K snd) (const1, const2))
   );
 
-type serializer =
-  string option                         (*module name*)
-  -> Token.T list                       (*arguments*)
+type serializer = Token.T list          (*arguments*)
   -> (string -> string)                 (*labelled_name*)
   -> string list                        (*reserved symbols*)
   -> (string * Pretty.T) list           (*includes*)
+  -> bool                               (*singleton module*)
   -> (string -> string option)          (*module aliasses*)
   -> (string -> string option)          (*class syntax*)
   -> (string -> Code_Printer.tyco_syntax option)
@@ -279,8 +278,8 @@
     val _ = if null empty_funs then () else error ("No code equations for "
       ^ commas (map (Sign.extern_const thy) empty_funs));
   in
-    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)
+    serializer args (Code_Thingol.labelled_name thy program2) reserved includes
+      (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias)
       (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
       program4 (names1, presentation_names) width
   end;