--- a/src/HOL/Library/code_test.ML Sun Sep 20 12:21:54 2020 +0200
+++ b/src/HOL/Library/code_test.ML Sun Sep 20 19:36:45 2020 +0200
@@ -18,13 +18,9 @@
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: (string * string) option -> string ->
- (Proof.context -> Path.T -> string list -> string ->
- {files: (Path.T * string) list,
- compile_cmd: string,
- run_cmd: string,
- mk_code_file: string -> Path.T}) -> Proof.context ->
- (string * string) list * string -> Path.T -> string
+ val check_settings: string -> string -> string -> unit
+ val compile: string -> string -> unit
+ val evaluate: string -> string -> 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
@@ -136,9 +132,9 @@
(ts ~~ evals))]
fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
- Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for")
- @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
- @ pretty_eval ctxt evals eval_ts)
+ Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @
+ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @
+ pretty_eval ctxt evals eval_ts)
fun pretty_failures ctxt target failures =
Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
@@ -231,8 +227,8 @@
handle ListPair.UnequalLengths =>
error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result))
in
- (case failed of [] =>
- ()
+ (case failed of
+ [] => ()
| _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
end
@@ -275,86 +271,62 @@
in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
-(* generic driver *)
+(* check and invoke compiler *)
-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) =>
- (case getenv env_var of
- "" =>
- error (Pretty.string_of (Pretty.para
- ("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 check_settings compiler var descr =
+ if getenv var = "" then
+ error (Pretty.string_of (Pretty.para
+ ("Environment variable " ^ var ^ " is not set. To test code generation with " ^
+ compiler ^ ", set this variable to your " ^ descr ^
+ " in the $ISABELLE_HOME_USER/etc/settings file.")))
+ else ();
- 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)
- end
+fun compile compiler cmd =
+ let val (out, ret) = Isabelle_System.bash_output cmd in
+ if ret = 0 then ()
+ else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out)
+ end
- fun run dir =
- let
- val modules = map fst code_files
- val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt dir modules value_name
-
- val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files
- val _ = List.app (fn (name, content) => File.write name content) files
-
- val _ = compile compile_cmd
-
- val (out, res) = Isabelle_System.bash_output run_cmd
- val _ =
- if res = 0 then ()
- else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
- string_of_int res ^ "\nCompiler output:\n" ^ out)
- in out end
- in run end
+fun evaluate compiler cmd =
+ let val (out, res) = Isabelle_System.bash_output cmd in
+ if res = 0 then out
+ else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^
+ string_of_int res ^ "\nCompiler output:\n" ^ out)
+ end
(* driver for PolyML *)
val polymlN = "PolyML"
-val evaluate_in_polyml =
- evaluate NONE polymlN
- (fn _ => fn dir => fn _ => fn value_name =>
- let
- val generatedN = "generated.sml"
- val driverN = "driver.sml"
-
- val code_path = Path.append dir (Path.basic generatedN)
- val driver_path = Path.append dir (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)
+fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir =
+ let
+ val compiler = polymlN
+ val code_path = Path.append dir (Path.basic "generated.sml")
+ val driver_path = Path.append dir (Path.basic "driver.sml")
+ 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
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ evaluate compiler cmd
+ end
(* driver for mlton *)
@@ -362,36 +334,34 @@
val mltonN = "MLton"
val ISABELLE_MLTON = "ISABELLE_MLTON"
-val evaluate_in_mlton =
- evaluate (SOME (ISABELLE_MLTON, "MLton executable")) mltonN
- (fn _ => fn dir => fn _ => fn value_name =>
- let
- val generatedN = "generated.sml"
- val driverN = "driver.sml"
- val projectN = "test"
- val ml_basisN = projectN ^ ".mlb"
+fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir =
+ let
+ val compiler = mltonN
+ val generatedN = "generated.sml"
+ val driverN = "driver.sml"
+ val projectN = "test"
- val code_path = Path.append dir (Path.basic generatedN)
- val driver_path = Path.append dir (Path.basic driverN)
- val ml_basis_path = Path.append dir (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 dir (Path.basic projectN)),
- mk_code_file = K code_path}
- end)
+ val code_path = Path.append dir (Path.basic generatedN)
+ val driver_path = Path.append dir (Path.basic driverN)
+ val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb"))
+ 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 cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path
+ in
+ check_settings compiler ISABELLE_MLTON "MLton executable";
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN);
+ compile compiler cmd;
+ evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN)))
+ end
(* driver for SML/NJ *)
@@ -399,43 +369,41 @@
val smlnjN = "SMLNJ"
val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
-val evaluate_in_smlnj =
- evaluate (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN
- (fn _ => fn dir => fn _ => fn value_name =>
- let
- val generatedN = "generated.sml"
- val driverN = "driver.sml"
+fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir =
+ let
+ val compiler = smlnjN
+ val generatedN = "generated.sml"
+ val driverN = "driver.sml"
- val code_path = Path.append dir (Path.basic generatedN)
- val driver_path = Path.append dir (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)
+ val code_path = Path.append dir (Path.basic generatedN)
+ val driver_path = Path.append dir (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 ();"
+ in
+ check_settings compiler ISABELLE_SMLNJ "SMLNJ executable";
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"")
+ end
(* driver for OCaml *)
@@ -443,39 +411,37 @@
val ocamlN = "OCaml"
val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
-val evaluate_in_ocaml =
- evaluate (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN
- (fn _ => fn dir => fn _ => fn value_name =>
- let
- val generatedN = "generated.ml"
- val driverN = "driver.ml"
+fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir =
+ let
+ val compiler = ocamlN
- val code_path = Path.append dir (Path.basic generatedN)
- val driver_path = Path.append dir (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 dir (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 dir ^ " " ^
- 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)
+ val code_path = Path.append dir (Path.basic "generated.ml")
+ val driver_path = Path.append dir (Path.basic "driver.ml")
+ 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 dir (Path.basic "test")
+ val cmd =
+ "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
+ " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^
+ File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
+ in
+ check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable";
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ compile compiler cmd;
+ evaluate compiler (File.bash_path compiled_path)
+ end
(* driver for GHC *)
@@ -485,85 +451,88 @@
val ghc_options = Attrib.setup_config_string \<^binding>\<open>code_test_ghc\<close> (K "")
-val evaluate_in_ghc =
- evaluate (SOME (ISABELLE_GHC, "GHC executable")) ghcN
- (fn ctxt => fn dir => fn modules => fn value_name =>
- let
- val driverN = "Main.hs"
+fun evaluate_in_ghc ctxt (code_files, value_name) dir =
+ let
+ val compiler = ghcN
+ val modules = map fst code_files
- fun mk_code_file name = Path.append dir (Path.basic name)
- val driver_path = Path.append dir (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 driver_path = Path.append dir (Path.basic "Main.hs")
+ 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 dir (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 dir),
- run_cmd = File.bash_path compiled_path,
- mk_code_file = mk_code_file}
- end)
+ val compiled_path = Path.append dir (Path.basic "test")
+ val 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 dir)
+ in
+ check_settings compiler ISABELLE_GHC "GHC executable";
+ List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files;
+ File.write driver_path driver;
+ compile compiler cmd;
+ evaluate compiler (File.bash_path compiled_path)
+ end
(* driver for Scala *)
val scalaN = "Scala"
-val evaluate_in_scala = evaluate NONE scalaN
- (fn _ => fn dir => fn _ => fn value_name =>
- let
- val generatedN = "Generated_Code"
- val driverN = "Driver.scala"
+fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir =
+ let
+ val compiler = scalaN
+ val generatedN = "Generated_Code"
+ val driverN = "Driver.scala"
- val code_path = Path.append dir (Path.basic (generatedN ^ ".scala"))
- val driver_path = Path.append dir (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 dir) ^
- " -classpath " ^ Bash.string (File.platform_path dir) ^ " " ^
- 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 dir) ^ " Test",
- mk_code_file = K code_path}
- end)
+ val code_path = Path.append dir (Path.basic (generatedN ^ ".scala"))
+ val driver_path = Path.append dir (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 dir) ^
+ " -classpath " ^ Bash.string (File.platform_path dir) ^ " " ^
+ 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 dir) ^ " Test"
+ in
+ List.app (File.write code_path o snd) code_files;
+ File.write driver_path driver;
+ compile compiler compile_cmd;
+ evaluate compiler run_cmd
+ end
(* command setup *)