--- 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;
--- 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*)
--- 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
--- 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 =