diff -r b8f30228a55b -r ad538f6c5d2f src/Tools/Code/code_ml.ML --- 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