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