make SML/NJ more happy;
authorwenzelm
Thu Oct 30 11:24:53 2014 +0100 (2014-10-30)
changeset 58832ec9550bd5fd7
parent 58831 aa8cf5eed06e
child 58833 09974789e483
child 58835 462ec23aa92f
make SML/NJ more happy;
src/HOL/Library/code_test.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Thu Oct 30 11:08:26 2014 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Thu Oct 30 11:24:53 2014 +0100
     1.3 @@ -348,7 +348,8 @@
     1.4      {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
     1.5    end
     1.6  
     1.7 -val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
     1.8 +fun evaluate_in_polyml ctxt =
     1.9 +  gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
    1.10  
    1.11  (* Driver for mlton *)
    1.12  
    1.13 @@ -388,7 +389,8 @@
    1.14       compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
    1.15    end
    1.16  
    1.17 -val evaluate_in_mlton = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN
    1.18 +fun evaluate_in_mlton ctxt =
    1.19 +  gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
    1.20  
    1.21  (* Driver for SML/NJ *)
    1.22  
    1.23 @@ -426,7 +428,8 @@
    1.24      {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
    1.25    end
    1.26  
    1.27 -val evaluate_in_smlnj = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN
    1.28 +fun evaluate_in_smlnj ctxt =
    1.29 +  gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
    1.30  
    1.31  (* Driver for OCaml *)
    1.32  
    1.33 @@ -466,7 +469,8 @@
    1.34       compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
    1.35    end
    1.36  
    1.37 -val evaluate_in_ocaml = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN
    1.38 +fun evaluate_in_ocaml ctxt =
    1.39 +  gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
    1.40  
    1.41  (* Driver for GHC *)
    1.42  
    1.43 @@ -510,7 +514,8 @@
    1.44       compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
    1.45    end
    1.46  
    1.47 -val evaluate_in_ghc = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN
    1.48 +fun evaluate_in_ghc ctxt =
    1.49 +  gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
    1.50  
    1.51  (* Driver for Scala *)
    1.52  
    1.53 @@ -556,7 +561,8 @@
    1.54       compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
    1.55    end
    1.56  
    1.57 -val evaluate_in_scala = gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN
    1.58 +fun evaluate_in_scala ctxt =
    1.59 +  gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
    1.60  
    1.61  val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
    1.62