# HG changeset patch
# User wenzelm
# Date 1300024298 -3600
# Node ID a3b68a7a0e1576cf1f8984392e58c1b65ee7f0d1
# Parent  eb9fb5a4d27fb58a6c011961626d735444fc4d34
allow spaces in executable names;
simplified generated bash scripts;

diff -r eb9fb5a4d27f -r a3b68a7a0e15 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 13:57:20 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 14:51:38 2011 +0100
@@ -782,17 +782,16 @@
 fun prelude system =
   case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
 
-fun invoke system file_name =
+fun invoke system file =
   let
-    val env_var =
-      (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP")
-    val prog = getenv env_var
-    val cmd =
-      case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L "
+    val (env_var, cmd) =
+      (case system of
+        SWI_PROLOG => ("EXEC_SWIPL", "\"$EXEC_SWIPL\" -f ")
+      | YAP => ("EXEC_YAP", "\"$EXEC_YAP\" -L "))
   in
-    if prog = "" then
+    if getenv env_var = "" then
       (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
-    else fst (bash_output (cmd ^ file_name))
+    else fst (bash_output (cmd ^ File.shell_path file))
   end
 
 (* parsing prolog solution *)
@@ -857,7 +856,7 @@
     val _ = tracing ("Generated prolog program:\n" ^ prog)
     val solution = TimeLimit.timeLimit timeout (fn prog =>
       Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
-        (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
+        (File.write prolog_file prog; invoke system prolog_file))) prog
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
     val tss = parse_solutions solution
   in
diff -r eb9fb5a4d27f -r a3b68a7a0e15 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 13:57:20 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 14:51:38 2011 +0100
@@ -43,7 +43,7 @@
         val _ = File.write narrowing_engine_file narrowing_engine
         val _ = File.write main_file main
         val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
-        val cmd = getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ 
+        val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^
           (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ " && " ^ executable
       in
diff -r eb9fb5a4d27f -r a3b68a7a0e15 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Mar 13 13:57:20 2011 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sun Mar 13 14:51:38 2011 +0100
@@ -453,8 +453,9 @@
   Code_Target.add_target
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "EXEC_GHC", make_destination = I,
-        make_command = fn ghc => fn module_name =>
-          ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
+        make_command = fn module_name =>
+          "\"$EXEC_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
+            module_name ^ ".hs" } })
   #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
diff -r eb9fb5a4d27f -r a3b68a7a0e15 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Mar 13 13:57:20 2011 +0100
+++ b/src/Tools/Code/code_ml.ML	Sun Mar 13 14:51:38 2011 +0100
@@ -836,12 +836,14 @@
 val setup =
   Code_Target.add_target
     (target_SML, { serializer = serializer_sml, literals = literals_sml,
-      check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
-        make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
+      check = { env_var = "ISABELLE_PROCESS",
+        make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
+        make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
   #> Code_Target.add_target
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
-      check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
-        make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
+      check = { env_var = "EXEC_OCAML",
+        make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
+        make_command = fn _ => "\"$EXEC_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
diff -r eb9fb5a4d27f -r a3b68a7a0e15 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Mar 13 13:57:20 2011 +0100
+++ b/src/Tools/Code/code_scala.ML	Sun Mar 13 14:51:38 2011 +0100
@@ -421,10 +421,8 @@
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "SCALA_HOME",
         make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
-        make_command = fn scala_home => fn _ =>
-          "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
-            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac"))
-            ^ " ROOT.scala" } })
+        make_command = fn _ =>
+          "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
   #> Code_Target.add_tyco_syntax target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (
diff -r eb9fb5a4d27f -r a3b68a7a0e15 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Mar 13 13:57:20 2011 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Mar 13 14:51:38 2011 +0100
@@ -35,8 +35,8 @@
   type serializer
   type literals = Code_Printer.literals
   val add_target: string * { serializer: serializer, literals: literals,
-    check: { env_var: string, make_destination: Path.T -> Path.T,
-      make_command: string -> string -> string } } -> theory -> theory
+    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
+    -> theory -> theory
   val extend_target: string *
       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
     -> theory -> theory
@@ -129,7 +129,7 @@
 datatype description = Fundamental of { serializer: serializer,
       literals: literals,
       check: { env_var: string, make_destination: Path.T -> Path.T,
-        make_command: string -> string -> string } }
+        make_command: string -> string } }
   | Extension of string *
       (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
 
@@ -392,18 +392,17 @@
     val module_name = "Code";
     val { env_var, make_destination, make_command } =
       (#check o the_fundamental thy) target;
-    val env_param = getenv env_var;
     fun ext_check p =
       let 
         val destination = make_destination p;
         val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
           module_name args naming program names_cs);
-        val cmd = make_command env_param module_name;
+        val cmd = make_command module_name;
       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
         else ()
       end;
-  in if env_param = ""
+  in if getenv env_var = ""
     then if strict
       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)