src/Tools/Code/code_ml.ML
changeset 51091 c007c6bf4a35
parent 50625 e3d25e751d05
child 51143 0a2371e7ced3
equal deleted inserted replaced
51090:bee2678a3b61 51091:c007c6bf4a35
   831   Code_Target.add_target
   831   Code_Target.add_target
   832     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   832     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   833       check = { env_var = "ISABELLE_PROCESS",
   833       check = { env_var = "ISABELLE_PROCESS",
   834         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   834         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   835         make_command = fn _ =>
   835         make_command = fn _ =>
   836           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' Pure" } })
   836           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   837   #> Code_Target.add_target
   837   #> Code_Target.add_target
   838     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   838     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   839       check = { env_var = "ISABELLE_OCAML",
   839       check = { env_var = "ISABELLE_OCAML",
   840         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   840         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   841         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   841         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })