src/HOL/Library/code_test.ML

   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 evaluate:
-   (theory -> Path.T -> string list -> string ->
+  val evaluate: (string * string) option -> string ->
+   (Proof.context -> Path.T -> string list -> string ->
      {files: (Path.T * string) list,
-       compile_cmd: string option,
+       compile_cmd: string,
        run_cmd: string,
-       mk_code_file: string -> Path.T}) -> (string * string) option -> string -> theory ->
+       mk_code_file: string -> Path.T}) -> Proof.context ->
      (string * string) list * string -> Path.T -> string
   val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string

       (case get_driver thy compiler of
         NONE => error ("No driver for target " ^ compiler)
       | SOME drv => drv)
     val debug = Config.get (Proof_Context.init_global thy) overlord
     val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
-    fun evaluate result =
+    fun eval result =
       with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
       |> parse_result compiler
     fun evaluator program _ vs_ty deps =
-      Exn.interruptible_capture evaluate
+      Exn.interruptible_capture eval
         (Code_Target.compilation_text ctxt target program deps true vs_ty)
     fun postproc f = map (apsnd (Option.map (map f)))
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
 

   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
 
 
 (* generic driver *)
 
-fun evaluate mk_driver opt_env_var compilerN ctxt (code_files, value_name) =
+fun evaluate opt_env_var compilerN mk_driver (ctxt: Proof.context) (code_files, value_name) =
   let
     val _ =
       (case opt_env_var of
         NONE => ()
       | SOME (env_var, env_var_dest) =>

                 ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
                   compilerN ^ ", set this variable to your " ^ env_var_dest ^
                   " in the $ISABELLE_HOME_USER/etc/settings file.")))
           | _ => ()))
 
-    fun compile NONE = ()
-      | compile (SOME cmd) =
+    fun compile "" = ()
+      | compile cmd =
           let
             val (out, ret) = Isabelle_System.bash_output cmd
           in
             if ret = 0 then ()
             else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)

 
 (* driver for PolyML *)
 
 val polymlN = "PolyML"
 
-fun mk_driver_polyml _ path _ value_name =
-  let
-    val generatedN = "generated.sml"
-    val driverN = "driver.sml"
-
-    val code_path = Path.append path (Path.basic generatedN)
-    val driver_path = Path.append path (Path.basic driverN)
-    val driver =
-      "fun main prog_name = \n" ^
-      "  let\n" ^
-      "    fun format_term NONE = \"\"\n" ^
-      "      | format_term (SOME t) = t ();\n" ^
-      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
-      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
-      "    val result = " ^ value_name ^ " ();\n" ^
-      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
-      "    val _ = map (print o format) result;\n" ^
-      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
-      "  in\n" ^
-      "    ()\n" ^
-      "  end;\n"
-    val cmd =
-      "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^
-      " --use " ^ Bash.string (File.platform_path driver_path) ^
-      " --eval " ^ Bash.string "main ()"
-  in
-    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
-  end
-
-fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt
+val evaluate_in_polyml =
+  evaluate NONE polymlN
+    (fn _ => fn path => fn _ => fn value_name =>
+      let
+        val generatedN = "generated.sml"
+        val driverN = "driver.sml"
+
+        val code_path = Path.append path (Path.basic generatedN)
+        val driver_path = Path.append path (Path.basic driverN)
+        val driver =
+          "fun main prog_name = \n" ^
+          "  let\n" ^
+          "    fun format_term NONE = \"\"\n" ^
+          "      | format_term (SOME t) = t ();\n" ^
+          "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
+          "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
+          "    val result = " ^ value_name ^ " ();\n" ^
+          "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
+          "    val _ = map (print o format) result;\n" ^
+          "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
+          "  in\n" ^
+          "    ()\n" ^
+          "  end;\n"
+      in
+       {files = [(driver_path, driver)],
+        compile_cmd = "",
+        run_cmd =
+          "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^
+          " --use " ^ Bash.string (File.platform_path driver_path) ^
+          " --eval " ^ Bash.string "main ()",
+        mk_code_file = K code_path}
+      end)
 
 
 (* driver for mlton *)
 
 val mltonN = "MLton"
 val ISABELLE_MLTON = "ISABELLE_MLTON"
 
-fun mk_driver_mlton _ path _ value_name =
-  let
-    val generatedN = "generated.sml"
-    val driverN = "driver.sml"
-    val projectN = "test"
-    val ml_basisN = projectN ^ ".mlb"
-
-    val code_path = Path.append path (Path.basic generatedN)
-    val driver_path = Path.append path (Path.basic driverN)
-    val ml_basis_path = Path.append path (Path.basic ml_basisN)
-    val driver =
-      "fun format_term NONE = \"\"\n" ^
-      "  | format_term (SOME t) = t ();\n" ^
-      "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
-      "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
-      "val result = " ^ value_name ^ " ();\n" ^
-      "val _ = print \"" ^ start_markerN ^ "\";\n" ^
-      "val _ = map (print o format) result;\n" ^
-      "val _ = print \"" ^ end_markerN ^ "\";\n"
-    val ml_basis =
-      "$(SML_LIB)/basis/basis.mlb\n" ^
-      generatedN ^ "\n" ^
-      driverN
-
-    val compile_cmd =
-      File.bash_path (Path.variable ISABELLE_MLTON) ^
-      " -default-type intinf " ^ File.bash_path ml_basis_path
-    val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
-  in
-    {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 =
-  evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt
+val evaluate_in_mlton =
+  evaluate (SOME (ISABELLE_MLTON, "MLton executable")) mltonN
+    (fn _ => fn path => fn _ => fn value_name =>
+      let
+        val generatedN = "generated.sml"
+        val driverN = "driver.sml"
+        val projectN = "test"
+        val ml_basisN = projectN ^ ".mlb"
+
+        val code_path = Path.append path (Path.basic generatedN)
+        val driver_path = Path.append path (Path.basic driverN)
+        val ml_basis_path = Path.append path (Path.basic ml_basisN)
+        val driver =
+          "fun format_term NONE = \"\"\n" ^
+          "  | format_term (SOME t) = t ();\n" ^
+          "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
+          "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
+          "val result = " ^ value_name ^ " ();\n" ^
+          "val _ = print \"" ^ start_markerN ^ "\";\n" ^
+          "val _ = map (print o format) result;\n" ^
+          "val _ = print \"" ^ end_markerN ^ "\";\n"
+        val ml_basis = "$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN
+      in
+       {files = [(driver_path, driver), (ml_basis_path, ml_basis)],
+        compile_cmd =
+          File.bash_path (Path.variable ISABELLE_MLTON) ^
+            " -default-type intinf " ^ File.bash_path ml_basis_path,
+        run_cmd = File.bash_path (Path.append path (Path.basic projectN)),
+        mk_code_file = K code_path}
+      end)
 
 
 (* driver for SML/NJ *)
 
 val smlnjN = "SMLNJ"
 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
 
-fun mk_driver_smlnj _ path _ value_name =
-  let
-    val generatedN = "generated.sml"
-    val driverN = "driver.sml"
-
-    val code_path = Path.append path (Path.basic generatedN)
-    val driver_path = Path.append path (Path.basic driverN)
-    val driver =
-      "structure Test = struct\n" ^
-      "fun main prog_name =\n" ^
-      "  let\n" ^
-      "    fun format_term NONE = \"\"\n" ^
-      "      | format_term (SOME t) = t ();\n" ^
-      "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
-      "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
-      "    val result = " ^ value_name ^ " ();\n" ^
-      "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
-      "    val _ = map (print o format) result;\n" ^
-      "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
-      "  in\n" ^
-      "    0\n" ^
-      "  end;\n" ^
-      "end;"
-    val ml_source =
-      "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
-      "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
-      "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
-      "; Test.main ();"
-    val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
-  in
-    {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
-  end
-
-fun evaluate_in_smlnj ctxt =
-  evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt
+val evaluate_in_smlnj =
+  evaluate (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN
+    (fn _ => fn path => fn _ => fn value_name =>
+      let
+        val generatedN = "generated.sml"
+        val driverN = "driver.sml"
+
+        val code_path = Path.append path (Path.basic generatedN)
+        val driver_path = Path.append path (Path.basic driverN)
+        val driver =
+          "structure Test = struct\n" ^
+          "fun main prog_name =\n" ^
+          "  let\n" ^
+          "    fun format_term NONE = \"\"\n" ^
+          "      | format_term (SOME t) = t ();\n" ^
+          "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
+          "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
+          "    val result = " ^ value_name ^ " ();\n" ^
+          "    val _ = print \"" ^ start_markerN ^ "\";\n" ^
+          "    val _ = map (print o format) result;\n" ^
+          "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
+          "  in\n" ^
+          "    0\n" ^
+          "  end;\n" ^
+          "end;"
+        val ml_source =
+          "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
+          "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
+          "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
+          "; Test.main ();"
+        val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
+      in
+       {files = [(driver_path, driver)],
+        compile_cmd = "",
+        run_cmd = cmd,
+        mk_code_file = K code_path}
+      end)
 
 
 (* driver for OCaml *)
 
 val ocamlN = "OCaml"
 val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
 
-fun mk_driver_ocaml _ path _ value_name =
-  let
-    val generatedN = "generated.ml"
-    val driverN = "driver.ml"
-
-    val code_path = Path.append path (Path.basic generatedN)
-    val driver_path = Path.append path (Path.basic driverN)
-    val driver =
-      "let format_term = function\n" ^
-      "  | None -> \"\"\n" ^
-      "  | Some t -> t ();;\n" ^
-      "let format = function\n" ^
-      "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
-      "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
-      "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
-      "let main x =\n" ^
-      "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
-      "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
-      "  print_string \"" ^ end_markerN ^ "\";;\n" ^
-      "main ();;"
-
-    val compiled_path = Path.append path (Path.basic "test")
-    val compile_cmd =
-      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
-      " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
-      File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
-
-    val run_cmd = File.bash_path compiled_path
-  in
-    {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 =
-  evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN ctxt
+val evaluate_in_ocaml =
+  evaluate (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN
+    (fn _ => fn path => fn _ => fn value_name =>
+      let
+        val generatedN = "generated.ml"
+        val driverN = "driver.ml"
+
+        val code_path = Path.append path (Path.basic generatedN)
+        val driver_path = Path.append path (Path.basic driverN)
+        val driver =
+          "let format_term = function\n" ^
+          "  | None -> \"\"\n" ^
+          "  | Some t -> t ();;\n" ^
+          "let format = function\n" ^
+          "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
+          "  | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
+          "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
+          "let main x =\n" ^
+          "  let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^
+          "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
+          "  print_string \"" ^ end_markerN ^ "\";;\n" ^
+          "main ();;"
+
+        val compiled_path = Path.append path (Path.basic "test")
+      in
+       {files = [(driver_path, driver)],
+        compile_cmd =
+          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
+          " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
+          File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null",
+        run_cmd = File.bash_path compiled_path,
+        mk_code_file = K code_path}
+      end)
 
 
 (* driver for GHC *)
 
 val ghcN = "GHC"
 val ISABELLE_GHC = "ISABELLE_GHC"
 
 val ghc_options = Attrib.setup_config_string \<^binding>\<open>code_test_ghc\<close> (K "")
 
-fun mk_driver_ghc ctxt path modules value_name =
-  let
-    val driverN = "Main.hs"
-
-    fun mk_code_file name = Path.append path (Path.basic name)
-    val driver_path = Path.append path (Path.basic driverN)
-    val driver =
-      "module Main where {\n" ^
-      implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
-      "main = do {\n" ^
-      "    let {\n" ^
-      "      format_term Nothing = \"\";\n" ^
-      "      format_term (Just t) = t ();\n" ^
-      "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
-      "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
-      "      result = " ^ value_name ^ " ();\n" ^
-      "    };\n" ^
-      "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
-      "    Prelude.mapM_ (putStr . format) result;\n" ^
-      "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
-      "  }\n" ^
-      "}\n"
-
-    val compiled_path = Path.append path (Path.basic "test")
-    val compile_cmd =
-      "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
-      Config.get ctxt ghc_options ^ " -o " ^ Bash.string (File.platform_path compiled_path) ^ " " ^
-      Bash.string (File.platform_path driver_path) ^ " -i" ^ Bash.string (File.platform_path path)
-
-    val run_cmd = File.bash_path compiled_path
-  in
-    {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 =
-  evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt
+val evaluate_in_ghc =
+  evaluate (SOME (ISABELLE_GHC, "GHC executable")) ghcN
+    (fn ctxt => fn path => fn modules => fn value_name =>
+      let
+        val driverN = "Main.hs"
+
+        fun mk_code_file name = Path.append path (Path.basic name)
+        val driver_path = Path.append path (Path.basic driverN)
+        val driver =
+          "module Main where {\n" ^
+          implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
+          "main = do {\n" ^
+          "    let {\n" ^
+          "      format_term Nothing = \"\";\n" ^
+          "      format_term (Just t) = t ();\n" ^
+          "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
+          "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
+          "      result = " ^ value_name ^ " ();\n" ^
+          "    };\n" ^
+          "    Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^
+          "    Prelude.mapM_ (putStr . format) result;\n" ^
+          "    Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^
+          "  }\n" ^
+          "}\n"
+
+        val compiled_path = Path.append path (Path.basic "test")
+      in
+       {files = [(driver_path, driver)],
+        compile_cmd =
+          "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
+          Config.get ctxt ghc_options ^ " -o " ^
+          Bash.string (File.platform_path compiled_path) ^ " " ^
+          Bash.string (File.platform_path driver_path) ^ " -i" ^
+          Bash.string (File.platform_path path),
+        run_cmd = File.bash_path compiled_path,
+        mk_code_file = mk_code_file}
+      end)
 
 
 (* driver for Scala *)
 
 val scalaN = "Scala"
 
-fun mk_driver_scala _ path _ value_name =
-  let
-    val generatedN = "Generated_Code"
-    val driverN = "Driver.scala"
-
-    val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
-    val driver_path = Path.append path (Path.basic driverN)
-    val driver =
-      "import " ^ generatedN ^ "._\n" ^
-      "object Test {\n" ^
-      "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
-      "    case None => \"\"\n" ^
-      "    case Some(x) => x(())\n" ^
-      "  }\n" ^
-      "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
-      "      case (true, _) => \"True\\n\"\n" ^
-      "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
-      "  }\n" ^
-      "  def main(args:Array[String]) = {\n" ^
-      "    val result = " ^ value_name ^ "(());\n" ^
-      "    print(\"" ^ start_markerN ^ "\");\n" ^
-      "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
-      "    print(\"" ^ end_markerN ^ "\");\n" ^
-      "  }\n" ^
-      "}\n"
-
-    val compile_cmd =
-      "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path path) ^
-      " -classpath " ^ Bash.string (File.platform_path path) ^ " " ^
-      Bash.string (File.platform_path code_path) ^ " " ^
-      Bash.string (File.platform_path driver_path)
-
-    val run_cmd = "isabelle_scala scala -cp " ^ Bash.string (File.platform_path path) ^ " Test"
-  in
-    {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 = evaluate mk_driver_scala NONE scalaN ctxt
+val evaluate_in_scala = evaluate NONE scalaN
+  (fn _ => fn path => fn _ => fn value_name =>
+    let
+      val generatedN = "Generated_Code"
+      val driverN = "Driver.scala"
+
+      val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
+      val driver_path = Path.append path (Path.basic driverN)
+      val driver =
+        "import " ^ generatedN ^ "._\n" ^
+        "object Test {\n" ^
+        "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
+        "    case None => \"\"\n" ^
+        "    case Some(x) => x(())\n" ^
+        "  }\n" ^
+        "  def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^
+        "      case (true, _) => \"True\\n\"\n" ^
+        "      case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^
+        "  }\n" ^
+        "  def main(args:Array[String]) = {\n" ^
+        "    val result = " ^ value_name ^ "(());\n" ^
+        "    print(\"" ^ start_markerN ^ "\");\n" ^
+        "    result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^
+        "    print(\"" ^ end_markerN ^ "\");\n" ^
+        "  }\n" ^
+        "}\n"
+    in
+     {files = [(driver_path, driver)],
+      compile_cmd =
+        "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path path) ^
+        " -classpath " ^ Bash.string (File.platform_path path) ^ " " ^
+        Bash.string (File.platform_path code_path) ^ " " ^
+        Bash.string (File.platform_path driver_path),
+      run_cmd = "isabelle_scala scala -cp " ^ Bash.string (File.platform_path path) ^ " Test",
+      mk_code_file = K code_path}
+    end)
 
 
 (* command setup *)
 
 val _ =