tuned signature -- suppress pointless exports;
authorwenzelm
Sat Dec 17 14:13:15 2016 +0100 (2016-12-17)
changeset 64581ee4b9cea7fb5
parent 64580 43ad19fbe9dc
child 64582 3d20ded18f14
tuned signature -- suppress pointless exports;
src/HOL/Library/code_test.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Sat Dec 17 14:09:39 2016 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Sat Dec 17 14:13:15 2016 +0100
     1.3 @@ -9,8 +9,6 @@
     1.4    val add_driver:
     1.5      string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
     1.6      theory -> theory
     1.7 -  val get_driver: theory -> string ->
     1.8 -    ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
     1.9    val overlord: bool Config.T
    1.10    val successN: string
    1.11    val failureN: string
    1.12 @@ -19,40 +17,20 @@
    1.13    val test_terms: Proof.context -> term list -> string -> unit
    1.14    val test_targets: Proof.context -> term list -> string list -> unit
    1.15    val test_code_cmd: string list -> string list -> Proof.context -> unit
    1.16 -
    1.17    val eval_term: string -> Proof.context -> term -> term
    1.18 -
    1.19 -  val gen_driver:
    1.20 +  val evaluate:
    1.21     (theory -> Path.T -> string list -> string ->
    1.22      {files: (Path.T * string) list,
    1.23       compile_cmd: string option,
    1.24       run_cmd: string,
    1.25       mk_code_file: string -> Path.T}) ->
    1.26     string -> string -> string -> theory -> (string * string) list * string -> Path.T -> string
    1.27 -
    1.28 -  val ISABELLE_POLYML: string
    1.29 -  val polymlN: string
    1.30    val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
    1.31 -
    1.32 -  val mltonN: string
    1.33 -  val ISABELLE_MLTON: string
    1.34    val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
    1.35 -
    1.36 -  val smlnjN: string
    1.37 -  val ISABELLE_SMLNJ: string
    1.38    val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
    1.39 -
    1.40 -  val ocamlN: string
    1.41 -  val ISABELLE_OCAMLC: string
    1.42    val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string
    1.43 -
    1.44 -  val ghcN: string
    1.45 -  val ISABELLE_GHC: string
    1.46    val ghc_options: string Config.T
    1.47    val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
    1.48 -
    1.49 -  val scalaN: string
    1.50 -  val ISABELLE_SCALA: string
    1.51    val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
    1.52  end
    1.53  
    1.54 @@ -295,7 +273,7 @@
    1.55  
    1.56  (* generic driver *)
    1.57  
    1.58 -fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
    1.59 +fun evaluate mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
    1.60    let
    1.61      val compiler = getenv env_var
    1.62      val _ =
    1.63 @@ -368,7 +346,7 @@
    1.64    end
    1.65  
    1.66  fun evaluate_in_polyml ctxt =
    1.67 -  gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
    1.68 +  evaluate mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
    1.69  
    1.70  
    1.71  (* driver for mlton *)
    1.72 @@ -410,7 +388,7 @@
    1.73    end
    1.74  
    1.75  fun evaluate_in_mlton ctxt =
    1.76 -  gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
    1.77 +  evaluate mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
    1.78  
    1.79  
    1.80  (* driver for SML/NJ *)
    1.81 @@ -450,7 +428,7 @@
    1.82    end
    1.83  
    1.84  fun evaluate_in_smlnj ctxt =
    1.85 -  gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
    1.86 +  evaluate mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
    1.87  
    1.88  
    1.89  (* driver for OCaml *)
    1.90 @@ -492,7 +470,7 @@
    1.91    end
    1.92  
    1.93  fun evaluate_in_ocaml ctxt =
    1.94 -  gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
    1.95 +  evaluate mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
    1.96  
    1.97  
    1.98  (* driver for GHC *)
    1.99 @@ -538,7 +516,7 @@
   1.100    end
   1.101  
   1.102  fun evaluate_in_ghc ctxt =
   1.103 -  gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
   1.104 +  evaluate mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
   1.105  
   1.106  
   1.107  (* driver for Scala *)
   1.108 @@ -586,7 +564,7 @@
   1.109    end
   1.110  
   1.111  fun evaluate_in_scala ctxt =
   1.112 -  gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
   1.113 +  evaluate mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
   1.114  
   1.115  
   1.116  (* command setup *)