839 check = { env_var = "ISABELLE_PROCESS", |
839 check = { env_var = "ISABELLE_PROCESS", |
840 make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
840 make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
841 make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } }) |
841 make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } }) |
842 #> Code_Target.add_target |
842 #> Code_Target.add_target |
843 (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, |
843 (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, |
844 check = { env_var = "EXEC_OCAML", |
844 check = { env_var = "ISABELLE_OCAML", |
845 make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), |
845 make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), |
846 make_command = fn _ => "\"$EXEC_OCAML\" -w pu nums.cma ROOT.ocaml" } }) |
846 make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } }) |
847 #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
847 #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
848 brackify_infix (1, R) fxy ( |
848 brackify_infix (1, R) fxy ( |
849 print_typ (INFX (1, X)) ty1, |
849 print_typ (INFX (1, X)) ty1, |
850 str "->", |
850 str "->", |
851 print_typ (INFX (1, R)) ty2 |
851 print_typ (INFX (1, R)) ty2 |