--- a/src/HOL/Library/code_test.ML Mon May 22 14:15:24 2017 +0200
+++ b/src/HOL/Library/code_test.ML Mon May 22 14:44:07 2017 +0200
@@ -421,10 +421,12 @@
" 0\n" ^
" end;\n" ^
"end;"
- val cmd =
- "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
- "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
- "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
+ val ml_source =
+ "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
+ "use " ^ ML_Syntax.print_string (Path.implode (Path.expand code_path)) ^
+ "; use " ^ ML_Syntax.print_string (Path.implode (Path.expand 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
@@ -461,9 +463,9 @@
val compiled_path = Path.append path (Path.basic "test")
val compile_cmd =
- Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
- " -I " ^ Path.implode path ^
- " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
+ "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
+ " -I " ^ File.bash_path path ^
+ " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path
val run_cmd = File.bash_path compiled_path
in
@@ -507,9 +509,9 @@
val compiled_path = Path.append path (Path.basic "test")
val compile_cmd =
- Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
- Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
- Path.implode driver_path ^ " -i" ^ Path.implode path
+ "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
+ Config.get ctxt ghc_options ^ " -o " ^ File.bash_path compiled_path ^ " " ^
+ File.bash_path driver_path ^ " -i" ^ File.bash_path path
val run_cmd = File.bash_path compiled_path
in