src/Tools/Code/code_ml.ML
changeset 70352 ce3c1d8791eb
parent 69950 dbc2426a600d
child 71798 fc4f9dad5292
equal deleted inserted replaced
70351:32b4e1aec5ca 70352:ce3c1d8791eb
   883         make_command = fn _ =>
   883         make_command = fn _ =>
   884           "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
   884           "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
   885       evaluation_args = []})
   885       evaluation_args = []})
   886   #> Code_Target.add_language
   886   #> Code_Target.add_language
   887     (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
   887     (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
   888       check = {env_var = "ISABELLE_OCAMLEXEC",
   888       check = {env_var = "ISABELLE_OCAMLFIND",
   889         make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
   889         make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
   890           (*extension demanded by OCaml compiler*),
   890           (*extension demanded by OCaml compiler*),
   891         make_command = fn _ =>
   891         make_command = fn _ =>
   892           "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
   892           "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
   893       evaluation_args = []})
   893       evaluation_args = []})