--- a/src/Tools/Code/code_ml.ML Thu Dec 14 21:40:43 2017 +0100
+++ b/src/Tools/Code/code_ml.ML Thu Dec 14 18:42:39 2017 +0100
@@ -872,16 +872,18 @@
val _ = Theory.setup
(Code_Target.add_language
- (target_SML, { serializer = serializer_sml, literals = literals_sml,
- check = { env_var = "",
+ (target_SML, {serializer = serializer_sml, literals = literals_sml,
+ check = {env_var = "",
make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
make_command = fn _ =>
- "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
+ "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
+ evaluation_args = []})
#> Code_Target.add_language
- (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
- check = { env_var = "ISABELLE_OCAML",
+ (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
+ check = {env_var = "ISABELLE_OCAML",
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
+ make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml"},
+ evaluation_args = []})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names