src/Tools/code/code_ml.ML
changeset 31327 ffa5356cc343
parent 31156 90fed3d4430f
child 31382 5c563b968832
equal deleted inserted replaced
31326:deddd77112b7 31327:ffa5356cc343
  1079       >> ml_code_datatype_antiq);
  1079       >> ml_code_datatype_antiq);
  1080 
  1080 
  1081 fun isar_seri_sml module_name =
  1081 fun isar_seri_sml module_name =
  1082   Code_Target.parse_args (Scan.succeed ())
  1082   Code_Target.parse_args (Scan.succeed ())
  1083   #> (fn () => serialize_ml target_SML
  1083   #> (fn () => serialize_ml target_SML
  1084       (SOME (use_text ML_Context.local_context (1, "generated code") false))
  1084       (SOME (use_text ML_Env.local_context (1, "generated code") false))
  1085       pr_sml_module pr_sml_stmt module_name);
  1085       pr_sml_module pr_sml_stmt module_name);
  1086 
  1086 
  1087 fun isar_seri_ocaml module_name =
  1087 fun isar_seri_ocaml module_name =
  1088   Code_Target.parse_args (Scan.succeed ())
  1088   Code_Target.parse_args (Scan.succeed ())
  1089   #> (fn () => serialize_ml target_OCaml NONE
  1089   #> (fn () => serialize_ml target_OCaml NONE