equal
deleted
inserted
replaced
440 |
440 |
441 |
441 |
442 (* driver for OCaml *) |
442 (* driver for OCaml *) |
443 |
443 |
444 val ocamlN = "OCaml" |
444 val ocamlN = "OCaml" |
445 val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT" |
445 val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND" |
446 |
446 |
447 fun mk_driver_ocaml _ path _ value_name = |
447 fun mk_driver_ocaml _ path _ value_name = |
448 let |
448 let |
449 val generatedN = "generated.ml" |
449 val generatedN = "generated.ml" |
450 val driverN = "driver.ml" |
450 val driverN = "driver.ml" |
465 " print_string \"" ^ end_markerN ^ "\";;\n" ^ |
465 " print_string \"" ^ end_markerN ^ "\";;\n" ^ |
466 "main ();;" |
466 "main ();;" |
467 |
467 |
468 val compiled_path = Path.append path (Path.basic "test") |
468 val compiled_path = Path.append path (Path.basic "test") |
469 val compile_cmd = |
469 val compile_cmd = |
470 "\"$ISABELLE_HOME/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^ |
470 "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg " ^ |
471 " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^ |
471 " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^ |
472 File.bash_path code_path ^ " " ^ File.bash_path driver_path |
472 File.bash_path code_path ^ " " ^ File.bash_path driver_path |
473 |
473 |
474 val run_cmd = File.bash_path compiled_path |
474 val run_cmd = File.bash_path compiled_path |
475 in |
475 in |
476 {files = [(driver_path, driver)], |
476 {files = [(driver_path, driver)], |
477 compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} |
477 compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} |
478 end |
478 end |
479 |
479 |
480 fun evaluate_in_ocaml ctxt = |
480 fun evaluate_in_ocaml ctxt = |
481 evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt |
481 evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN ctxt |
482 |
482 |
483 |
483 |
484 (* driver for GHC *) |
484 (* driver for GHC *) |
485 |
485 |
486 val ghcN = "GHC" |
486 val ghcN = "GHC" |