--- a/src/Tools/Code/code_ml.ML Tue Dec 08 13:41:37 2009 +0100
+++ b/src/Tools/Code/code_ml.ML Tue Dec 08 14:31:19 2009 +0100
@@ -7,7 +7,7 @@
signature CODE_ML =
sig
val target_SML: string
- val evaluation_code_of: theory -> string -> string option
+ val evaluation_code_of: theory -> string -> string
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val setup: theory -> theory
end;
@@ -339,7 +339,9 @@
end;
in print_stmt end;
-fun print_sml_module name some_decls body = Pretty.chunks2 (
+fun print_sml_module name some_decls body = if name = ""
+ then Pretty.chunks2 body
+ else Pretty.chunks2 (
Pretty.chunks (
str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
:: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -663,7 +665,9 @@
end;
in print_stmt end;
-fun print_ocaml_module name some_decls body = Pretty.chunks2 (
+fun print_ocaml_module name some_decls body = if name = ""
+ then Pretty.chunks2 body
+ else Pretty.chunks2 (
Pretty.chunks (
str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
:: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -938,13 +942,9 @@
(** for instrumentalization **)
-fun evaluation_code_of thy target some_struct_name =
- let
- val serialize = if is_some some_struct_name then fn _ => fn [] =>
- serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt some_struct_name true
- else fn _ => fn [] =>
- serialize_ml target (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt some_struct_name true;
- in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
+fun evaluation_code_of thy target struct_name =
+ Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
+ serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
(** Isar setup **)