# HG changeset patch
# User wenzelm
# Date 1481982461 -3600
# Node ID 3d20ded18f14e5c8549083cb563f12e039ca85b3
# Parent  ee4b9cea7fb500ec4f351dca582effbf11827343
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;

diff -r ee4b9cea7fb5 -r 3d20ded18f14 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Sat Dec 17 14:13:15 2016 +0100
+++ b/src/HOL/Library/code_test.ML	Sat Dec 17 14:47:41 2016 +0100
@@ -20,11 +20,11 @@
   val eval_term: string -> Proof.context -> term -> term
   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
+     {files: (Path.T * string) list,
+       compile_cmd: string option,
+       run_cmd: string,
+       mk_code_file: string -> Path.T}) -> (string * string) option -> string -> theory ->
+     (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
@@ -273,15 +273,19 @@
 
 (* generic driver *)
 
-fun evaluate mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
+fun evaluate mk_driver opt_env_var compilerN ctxt (code_files, value_name) =
   let
-    val compiler = getenv env_var
     val _ =
-      if compiler <> "" then ()
-      else 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.")))
+      (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 compile NONE = ()
       | compile (SOME cmd) =
@@ -313,7 +317,6 @@
 
 (* driver for PolyML *)
 
-val ISABELLE_POLYML = "ISABELLE_POLYML"
 val polymlN = "PolyML"
 
 fun mk_driver_polyml _ path _ value_name =
@@ -339,14 +342,12 @@
       "  end;\n"
     val cmd =
       "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
-      Path.implode driver_path ^ "\\\"; main ();\" | " ^
-      Path.implode (Path.variable ISABELLE_POLYML)
+      Path.implode driver_path ^ "\\\"; main ();\" | \"$ML_HOME/poly\""
   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 ISABELLE_POLYML "PolyML executable" polymlN ctxt
+fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt
 
 
 (* driver for mlton *)
@@ -388,7 +389,7 @@
   end
 
 fun evaluate_in_mlton ctxt =
-  evaluate mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
+  evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt
 
 
 (* driver for SML/NJ *)
@@ -428,7 +429,7 @@
   end
 
 fun evaluate_in_smlnj ctxt =
-  evaluate mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
+  evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt
 
 
 (* driver for OCaml *)
@@ -470,7 +471,7 @@
   end
 
 fun evaluate_in_ocaml ctxt =
-  evaluate mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
+  evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
 
 
 (* driver for GHC *)
@@ -516,13 +517,12 @@
   end
 
 fun evaluate_in_ghc ctxt =
-  evaluate mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
+  evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt
 
 
 (* driver for Scala *)
 
 val scalaN = "Scala"
-val ISABELLE_SCALA = "ISABELLE_SCALA"
 
 fun mk_driver_scala _ path _ value_name =
   let
@@ -551,20 +551,17 @@
       "}\n"
 
     val compile_cmd =
-      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
-      " -d " ^ File.bash_path path ^ " -classpath " ^ File.bash_path path ^ " " ^
+      "\"$SCALA_HOME/bin/scalac\" -d " ^ File.bash_path path ^
+      " -classpath " ^ File.bash_path path ^ " " ^
       File.bash_path code_path ^ " " ^ File.bash_path driver_path
 
-    val run_cmd =
-      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
-      " -cp " ^ File.bash_path path ^ " Test"
+    val run_cmd = "\"$SCALA_HOME/bin/scala\" -cp " ^ File.bash_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 ISABELLE_SCALA "Scala directory" scalaN ctxt
+fun evaluate_in_scala ctxt = evaluate mk_driver_scala NONE scalaN ctxt
 
 
 (* command setup *)
diff -r ee4b9cea7fb5 -r 3d20ded18f14 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Dec 17 14:13:15 2016 +0100
+++ b/src/HOL/ROOT	Sat Dec 17 14:47:41 2016 +0100
@@ -238,16 +238,14 @@
     Generate_Target_Nat
     Generate_Efficient_Datastructures
     Generate_Pretty_Char
+    Code_Test_PolyML
+    Code_Test_Scala
   theories [condition = "ISABELLE_GHC"]
     Code_Test_GHC
   theories [condition = "ISABELLE_MLTON"]
     Code_Test_MLton
   theories [condition = "ISABELLE_OCAMLC"]
     Code_Test_OCaml
-  theories [condition = "ISABELLE_POLYML"]
-    Code_Test_PolyML
-  theories [condition = "ISABELLE_SCALA"]
-    Code_Test_Scala
   theories [condition = "ISABELLE_SMLNJ"]
     Code_Test_SMLNJ