# HG changeset patch
# User haftmann
# Date 1283257266 -7200
# Node ID 24f82786cc570459ebab952891fcfc919d411925
# Parent  ced825abdc1de0af89e5452e563355639684e89e
record argument for serializers

diff -r ced825abdc1d -r 24f82786cc57 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Aug 31 14:06:20 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Aug 31 14:21:06 2010 +0200
@@ -313,12 +313,12 @@
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
-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) =
+fun serialize_haskell module_prefix string_classes { labelled_name,
+    reserved_syms, includes, single_module, module_alias,
+    class_syntax, tyco_syntax, const_syntax, program,
+    names, presentation_names } =
   let
-    val reserved = fold (insert (op =) o fst) includes raw_reserved;
+    val reserved = fold (insert (op =) o fst) includes reserved_syms;
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
       module_prefix reserved module_alias program;
     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
@@ -368,13 +368,13 @@
           );
       in print_module module_name' content end;
     fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
-        (fn (name, (_, SOME stmt)) => if null presentation_stmt_names
-              orelse member (op =) presentation_stmt_names name
+        (fn (name, (_, SOME stmt)) => if null presentation_names
+              orelse member (op =) presentation_names name
               then SOME (print_stmt false (name, stmt))
               else NONE
           | (_, (_, NONE)) => NONE) stmts);
     val serialize_module =
-      if null presentation_stmt_names then serialize_module1 else pair "" o serialize_module2;
+      if null presentation_names then serialize_module1 else pair "" o serialize_module2;
     fun write_module width (SOME destination) (modlname, content) =
           let
             val _ = File.check destination;
diff -r ced825abdc1d -r 24f82786cc57 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Aug 31 14:06:20 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 14:21:06 2010 +0200
@@ -902,19 +902,19 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-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) =
+fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
+  reserved_syms, includes, single_module, module_alias, class_syntax, tyco_syntax,
+  const_syntax, program, names, presentation_names } =
   let
     val is_cons = Code_Thingol.is_cons program;
-    val is_presentation = not (null presentation_stmt_names);
+    val is_presentation = not (null presentation_names);
     val (deresolver, nodes) = ml_node_of_program labelled_name
-      reserved module_alias program;
-    val reserved = make_vars reserved;
+      reserved_syms module_alias program;
+    val reserved = make_vars reserved_syms;
     fun print_node prefix (Dummy _) =
           NONE
       | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
-          (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
+          (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
           then NONE
           else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
       | print_node prefix (Module (module_name, (_, nodes))) =
@@ -927,13 +927,13 @@
         o rev o flat o Graph.strong_conn) nodes
       |> split_list
       |> (fn (decls, body) => (flat decls, body))
-    val stmt_names' = map (try (deresolver [])) stmt_names
+    val names' = map (try (deresolver [])) 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;
   in
-    Code_Target.serialization write (fn width => (rpair stmt_names' o string_of_pretty width)) p
+    Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
   end;
 
 end; (*local*)
diff -r ced825abdc1d -r 24f82786cc57 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Aug 31 14:06:20 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Aug 31 14:21:06 2010 +0200
@@ -413,13 +413,13 @@
 
   in (deresolver, sca_program) end;
 
-fun serialize_scala labelled_name raw_reserved includes _ module_alias
-    _ tyco_syntax const_syntax
-    program (stmt_names, presentation_stmt_names) =
+fun serialize_scala { labelled_name, reserved_syms, includes, single_module,
+    module_alias, class_syntax, tyco_syntax, const_syntax, program,
+    names, presentation_names } =
   let
 
     (* build program *)
-    val reserved = fold (insert (op =) o fst) includes raw_reserved;
+    val reserved = fold (insert (op =) o fst) includes reserved_syms;
     val (deresolver, sca_program) = scala_program_of_program labelled_name
       (Name.make_context reserved) module_alias program;
 
@@ -455,12 +455,12 @@
       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
     fun print_node _ (_, Dummy) = NONE
       | print_node prefix_fragments (name, Stmt stmt) =
-          if null presentation_stmt_names
-          orelse member (op =) presentation_stmt_names name
+          if null presentation_names
+          orelse member (op =) presentation_names name
           then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
           else NONE
       | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
-          if null presentation_stmt_names
+          if null presentation_names
           then
             let
               val prefix_fragments' = prefix_fragments @ [name_fragment];
@@ -477,7 +477,7 @@
       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
 
     (* serialization *)
-    val p_includes = if null presentation_stmt_names
+    val p_includes = if null presentation_names
       then map (fn (base, p) => print_module base [] p) includes else [];
     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
     fun write width NONE = writeln_pretty width
diff -r ced825abdc1d -r 24f82786cc57 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Aug 31 14:06:20 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Aug 31 14:21:06 2010 +0200
@@ -101,17 +101,18 @@
        Symtab.join (K snd) (const1, const2))
   );
 
-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)
-  -> (string -> Code_Printer.activated_const_syntax option)
-  -> Code_Thingol.program
-  -> (string list * string list)        (*selected statements*)
+type serializer = Token.T list (*arguments*) -> {
+    labelled_name: string -> string,
+    reserved_syms: string list,
+    includes: (string * Pretty.T) list,
+    single_module: bool,
+    module_alias: string -> string option,
+    class_syntax: string -> string option,
+    tyco_syntax: string -> Code_Printer.tyco_syntax option,
+    const_syntax: string -> Code_Printer.activated_const_syntax option,
+    program: Code_Thingol.program,
+    names: string list,
+    presentation_names: string list }
   -> serialization;
 
 datatype description = Fundamental of { serializer: serializer,
@@ -277,10 +278,18 @@
     val _ = if null empty_funs then () else error ("No code equations for "
       ^ commas (map (Sign.extern_const thy) empty_funs));
   in
-    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
+    serializer args {
+      labelled_name = Code_Thingol.labelled_name thy program2,
+      reserved_syms = reserved,
+      includes = includes,
+      single_module = is_some module_name,
+      module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
+      class_syntax = Symtab.lookup class',
+      tyco_syntax = Symtab.lookup tyco',
+      const_syntax = Symtab.lookup const',
+      program = program3,
+      names = names1,
+      presentation_names = presentation_names } width
   end;
 
 fun mount_serializer thy target some_width raw_module_name args naming program names destination =