866 ); |
866 ); |
867 |
867 |
868 val _ = Theory.setup |
868 val _ = Theory.setup |
869 (Code_Target.add_language |
869 (Code_Target.add_language |
870 (target_SML, { serializer = serializer_sml, literals = literals_sml, |
870 (target_SML, { serializer = serializer_sml, literals = literals_sml, |
871 check = { env_var = "ISABELLE_PROCESS", |
871 check = { env_var = "ISABELLE_TOOL", |
872 make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
872 make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
873 make_command = fn _ => |
873 make_command = fn _ => |
874 "\"$ISABELLE_PROCESS\" -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } }) |
874 "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } }) |
875 #> Code_Target.add_language |
875 #> Code_Target.add_language |
876 (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, |
876 (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, |
877 check = { env_var = "ISABELLE_OCAML", |
877 check = { env_var = "ISABELLE_OCAML", |
878 make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), |
878 make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), |
879 make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } }) |
879 make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } }) |