src/Tools/Code/code_ml.ML
changeset 69926 110fff287217
parent 69910 0c0f7b4a72bf
child 69950 dbc2426a600d
equal deleted inserted replaced
69925:c90678ad942d 69926:110fff287217
   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_OCAMLEXEC",
   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_OCAMLEXEC\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
   892           "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
   893       evaluation_args = []})
   893       evaluation_args = []})
   894   #> Code_Target.set_printings (Type_Constructor ("fun",
   894   #> Code_Target.set_printings (Type_Constructor ("fun",
   895     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   895     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   896   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   896   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   897   #> fold (Code_Target.add_reserved target_SML)
   897   #> fold (Code_Target.add_reserved target_SML)