src/HOL/Library/code_test.ML

 signature CODE_TEST =
 sig
   val add_driver:
     string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
     theory -> theory
-  val get_driver: theory -> string ->
-    ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
   val overlord: bool Config.T
   val successN: string
   val failureN: string
   val start_markerN: string
   val end_markerN: string
   val test_terms: Proof.context -> term list -> string -> unit
   val test_targets: Proof.context -> term list -> string list -> unit
   val test_code_cmd: string list -> string list -> Proof.context -> unit
-
   val eval_term: string -> Proof.context -> term -> term
-
-  val gen_driver:
+  val evaluate:
    (theory -> Path.T -> string list -> string ->
     {files: (Path.T * string) list,
      compile_cmd: string option,
      run_cmd: string,
      mk_code_file: string -> Path.T}) ->
    string -> string -> string -> theory -> (string * string) list * string -> Path.T -> string
-
-  val ISABELLE_POLYML: string
-  val polymlN: string
   val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
-
-  val mltonN: string
-  val ISABELLE_MLTON: string
   val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
-
-  val smlnjN: string
-  val ISABELLE_SMLNJ: string
   val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
-
-  val ocamlN: string
-  val ISABELLE_OCAMLC: string
   val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string
-
-  val ghcN: string
-  val ISABELLE_GHC: string
   val ghc_options: string Config.T
   val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
-
-  val scalaN: string
-  val ISABELLE_SCALA: string
   val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
 end
 
 structure Code_Test: CODE_TEST =
 struct

   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
 
 
 (* generic driver *)
 
-fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
+fun evaluate mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
   let
     val compiler = getenv env_var
     val _ =
       if compiler <> "" then ()
       else error (Pretty.string_of (Pretty.para

   in
     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   end
 
 fun evaluate_in_polyml ctxt =
-  gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
+  evaluate mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
 
 
 (* driver for mlton *)
 
 val mltonN = "MLton"

     {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   end
 
 fun evaluate_in_mlton ctxt =
-  gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
+  evaluate mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
 
 
 (* driver for SML/NJ *)
 
 val smlnjN = "SMLNJ"

   in
     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   end
 
 fun evaluate_in_smlnj ctxt =
-  gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
+  evaluate mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
 
 
 (* driver for OCaml *)
 
 val ocamlN = "OCaml"

     {files = [(driver_path, driver)],
      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   end
 
 fun evaluate_in_ocaml ctxt =
-  gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
+  evaluate mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
 
 
 (* driver for GHC *)
 
 val ghcN = "GHC"

     {files = [(driver_path, driver)],
      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   end
 
 fun evaluate_in_ghc ctxt =
-  gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
+  evaluate mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
 
 
 (* driver for Scala *)
 
 val scalaN = "Scala"

     {files = [(driver_path, driver)],
      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   end
 
 fun evaluate_in_scala ctxt =
-  gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
+  evaluate mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
 
 
 (* command setup *)
 
 val _ =