# HG changeset patch
# User wenzelm
# Date 1411373921 -7200
# Node ID 8392d221bd91edb41c0c65cf08f578de0f29da25
# Parent  22dd971f6938bfd00dce20951f8bd3b70896c0f2
clarified ISABELLE_POLYML;
added some isatests -- ISABELLE_SCALA still inactive due to problems with case-insensible file-system;

diff -r 22dd971f6938 -r 8392d221bd91 Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Sun Sep 21 20:22:12 2014 +0200
+++ b/Admin/isatest/settings/mac-poly-M4	Mon Sep 22 10:18:41 2014 +0200
@@ -8,8 +8,6 @@
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 500 --gcthreads 4"
 
-ISABELLE_GHC=ghc
-
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
@@ -30,5 +28,13 @@
 
 ISABELLE_FULL_TEST=true
 
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
+
 Z3_NON_COMMERCIAL="yes"
 
diff -r 22dd971f6938 -r 8392d221bd91 Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Sun Sep 21 20:22:12 2014 +0200
+++ b/Admin/isatest/settings/mac-poly-M8	Mon Sep 22 10:18:41 2014 +0200
@@ -8,8 +8,6 @@
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-H 500 --gcthreads 8"
 
-ISABELLE_GHC=ghc
-
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
@@ -30,5 +28,13 @@
 
 ISABELLE_FULL_TEST=true
 
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
+
 Z3_NON_COMMERCIAL="yes"
 
diff -r 22dd971f6938 -r 8392d221bd91 src/HOL/Codegenerator_Test/code_test.ML
--- a/src/HOL/Codegenerator_Test/code_test.ML	Sun Sep 21 20:22:12 2014 +0200
+++ b/src/HOL/Codegenerator_Test/code_test.ML	Mon Sep 22 10:18:41 2014 +0200
@@ -25,7 +25,7 @@
    -> string -> string -> string
    -> theory -> (string * string) list * string -> Path.T -> string
 
-  val ISABELLE_POLYML_PATH : string
+  val ISABELLE_POLYML : string
   val polymlN : string
   val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
 
@@ -316,7 +316,7 @@
 
 (* Driver for PolyML *)
 
-val ISABELLE_POLYML_PATH = "ISABELLE_POLYML_PATH"
+val ISABELLE_POLYML = "ISABELLE_POLYML"
 val polymlN = "PolyML";
 
 fun mk_driver_polyml _ path _ value_name =
@@ -343,12 +343,12 @@
     val cmd =
       "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
       Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
-      Path.implode (Path.variable ISABELLE_POLYML_PATH)
+      Path.implode (Path.variable ISABELLE_POLYML)
   in
     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   end
 
-val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML_PATH "PolyML executable" polymlN
+val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
 
 (* Driver for mlton *)
 
diff -r 22dd971f6938 -r 8392d221bd91 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Sep 21 20:22:12 2014 +0200
+++ b/src/HOL/ROOT	Mon Sep 22 10:18:41 2014 +0200
@@ -242,17 +242,17 @@
     Generate_Efficient_Datastructures
     Generate_Pretty_Char
     Code_Test
-  theories[condition = ISABELLE_GHC]
+  theories [condition = ISABELLE_GHC]
     Code_Test_GHC
-  theories[condition = ISABELLE_MLTON]
+  theories [condition = ISABELLE_MLTON]
     Code_Test_MLton
-  theories[condition = ISABELLE_OCAMLC]
+  theories [condition = ISABELLE_OCAMLC]
     Code_Test_OCaml
-  theories[condition = ISABELLE_POLYML_PATH]
+  theories [condition = ISABELLE_POLYML]
     Code_Test_PolyML
-  theories[condition = ISABELLE_SCALA]
+  theories [condition = ISABELLE_SCALA]
     Code_Test_Scala
-  theories[condition = ISABELLE_SMLNJ]
+  theories [condition = ISABELLE_SMLNJ]
     Code_Test_SMLNJ
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +