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 _ => Posix.Process.exit 0w1' Pure" } }) |
836 "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 0' 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" } }) |