equal
deleted
inserted
replaced
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 |