src/Tools/Code/code_ml.ML
changeset 55683 5732a55b9232
parent 55682 def6575032df
child 55684 ee49b4f7edc8
equal deleted inserted replaced
55682:def6575032df 55683:5732a55b9232
   795       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
   795       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts }
   796   end;
   796   end;
   797 
   797 
   798 fun serialize_ml print_ml_module print_ml_stmt ctxt
   798 fun serialize_ml print_ml_module print_ml_stmt ctxt
   799     { module_name, reserved_syms, identifiers, includes,
   799     { module_name, reserved_syms, identifiers, includes,
   800       class_syntax, tyco_syntax, const_syntax } program =
   800       class_syntax, tyco_syntax, const_syntax } exports program =
   801   let
   801   let
   802 
   802 
   803     (* build program *)
   803     (* build program *)
   804     val { deresolver, hierarchical_program = ml_program } =
   804     val { deresolver, hierarchical_program = ml_program } =
   805       ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
   805       ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
   806         identifiers program;
   806         identifiers exports program;
   807 
   807 
   808     (* print statements *)
   808     (* print statements *)
   809     fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
   809     fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
   810       tyco_syntax const_syntax (make_vars reserved_syms)
   810       tyco_syntax const_syntax (make_vars reserved_syms)
   811       (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt
   811       (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt