proper passing of optional module name
authorhaftmann
Thu Aug 26 20:14:24 2010 +0200 (2010-08-26)
changeset 387843b4d63ab03c4
parent 38782 3865cbe5d2be
child 38785 afcc1fcb376b
proper passing of optional module name
src/Tools/Code/code_ml.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Aug 26 14:04:13 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 20:14:24 2010 +0200
     1.3 @@ -946,8 +946,8 @@
     1.4  (** for instrumentalization **)
     1.5  
     1.6  fun evaluation_code_of thy target struct_name =
     1.7 -  Code_Target.serialize_custom thy (target, fn _ => fn [] =>
     1.8 -    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
     1.9 +  Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
    1.10 +    serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
    1.11  
    1.12  
    1.13  (** Isar setup **)
     2.1 --- a/src/Tools/Code/code_target.ML	Thu Aug 26 14:04:13 2010 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Thu Aug 26 20:14:24 2010 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4      -> 'a -> serialization
     2.5    val serialize: theory -> string -> int option -> string option -> Token.T list
     2.6      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
     2.7 -  val serialize_custom: theory -> string * serializer
     2.8 +  val serialize_custom: theory -> string * serializer -> string option
     2.9      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    2.10    val the_literals: theory -> string -> literals
    2.11    val export: serialization -> unit
    2.12 @@ -348,8 +348,8 @@
    2.13      else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    2.14    end;
    2.15  
    2.16 -fun serialize_custom thy (target_name, seri) naming program names =
    2.17 -  mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
    2.18 +fun serialize_custom thy (target_name, seri) module_name naming program names =
    2.19 +  mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
    2.20    |> the;
    2.21  
    2.22  end; (* local *)