# HG changeset patch # User wenzelm # Date 1414664693 -3600 # Node ID ec9550bd5fd735dddcd6ac38906476a48fc03377 # Parent aa8cf5eed06ed85eb2ca2b07bc0686fa19802997 make SML/NJ more happy; diff -r aa8cf5eed06e -r ec9550bd5fd7 src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Thu Oct 30 11:08:26 2014 +0100 +++ b/src/HOL/Library/code_test.ML Thu Oct 30 11:24:53 2014 +0100 @@ -348,7 +348,8 @@ {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} end -val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN +fun evaluate_in_polyml ctxt = + gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt (* Driver for mlton *) @@ -388,7 +389,8 @@ compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} end -val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN +fun evaluate_in_mlton ctxt = + gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt (* Driver for SML/NJ *) @@ -426,7 +428,8 @@ {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} end -val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN +fun evaluate_in_smlnj ctxt = + gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt (* Driver for OCaml *) @@ -466,7 +469,8 @@ compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} end -val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN +fun evaluate_in_ocaml ctxt = + gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt (* Driver for GHC *) @@ -510,7 +514,8 @@ compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file} end -val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN +fun evaluate_in_ghc ctxt = + gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt (* Driver for Scala *) @@ -556,7 +561,8 @@ compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} end -val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN +fun evaluate_in_scala ctxt = + gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)