src/Tools/Code/code_ml.ML
changeset 39142 f63715f00fdd
parent 39102 4ae1d212100f
child 39148 b6530978c14d
equal deleted inserted replaced
39141:5ec8e4404c33 39142:f63715f00fdd
   783     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   783     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   784       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   784       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   785       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   785       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   786   end;
   786   end;
   787 
   787 
   788 fun serialize_ml target print_module print_stmt with_signatures { labelled_name,
   788 fun serialize_ml target print_module print_stmt with_signatures
   789   reserved_syms, includes, module_alias, class_syntax, tyco_syntax,
   789     { labelled_name, reserved_syms, includes, module_alias,
   790   const_syntax, program, names } =
   790       class_syntax, tyco_syntax, const_syntax, program } =
   791   let
   791   let
   792     val is_cons = Code_Thingol.is_cons program;
   792     val is_cons = Code_Thingol.is_cons program;
   793     val { deresolver, hierarchical_program = ml_program } =
   793     val { deresolver, hierarchical_program = ml_program } =
   794       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   794       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   795     val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
   795     val print_stmt = print_stmt labelled_name tyco_syntax const_syntax