File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
clarified treatment of whitespace in some bash scripts;
--- a/NEWS Mon Mar 07 20:44:47 2016 +0100
+++ b/NEWS Mon Mar 07 21:09:28 2016 +0100
@@ -213,6 +213,14 @@
*** System ***
+* File.bash_string, File.bash_path etc. represent Isabelle/ML and
+Isabelle/Scala strings authentically within GNU bash. This is useful to
+produce robust shell scripts under program control, without worrying
+about spaces or special characters. Note that user output works via
+Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
+less versatile) operations File.shell_quote, File.shell_path etc. have
+been discontinued.
+
* The Isabelle system environment always ensures that the main
executables are found within the PATH: isabelle, isabelle_process,
isabelle_scala_script.
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Mon Mar 07 21:09:28 2016 +0100
@@ -51,9 +51,10 @@
local
-fun make_cmd command options problem_path proof_path = space_implode " " (
- "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
- [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
+fun make_cmd command options problem_path proof_path =
+ space_implode " "
+ ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
fun trace_and ctxt msg f x =
let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) ()
@@ -82,7 +83,7 @@
Cache_IO.run_and_cache certs key mk_cmd input
| (SOME output, _) =>
trace_and ctxt ("Using cached certificate from " ^
- File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
+ Path.print (Cache_IO.cache_path_of certs) ^ " ...")
I output))
fun run_solver ctxt name mk_cmd input =
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Mar 07 21:09:28 2016 +0100
@@ -40,7 +40,7 @@
val (output, rc) =
Isabelle_System.bash_output
- ("\"$ISABELLE_CSDP\" " ^ File.shell_path in_path ^ " " ^ File.shell_path out_path)
+ ("\"$ISABELLE_CSDP\" " ^ File.bash_path in_path ^ " " ^ File.bash_path out_path)
val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
val result = if File.exists out_path then File.read out_path else ""
--- a/src/HOL/Library/code_test.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Library/code_test.ML Mon Mar 07 21:09:28 2016 +0100
@@ -382,9 +382,9 @@
driverN
val compile_cmd =
- File.shell_path (Path.variable ISABELLE_MLTON) ^
- " -default-type intinf " ^ File.shell_path ml_basis_path
- val run_cmd = File.shell_path (Path.append path (Path.basic projectN))
+ File.bash_path (Path.variable ISABELLE_MLTON) ^
+ " -default-type intinf " ^ File.bash_path ml_basis_path
+ val run_cmd = File.bash_path (Path.append path (Path.basic projectN))
in
{files = [(driver_path, driver), (ml_basis_path, ml_basis)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
@@ -464,7 +464,7 @@
" -I " ^ Path.implode path ^
" nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
- val run_cmd = File.shell_path compiled_path
+ val run_cmd = File.bash_path compiled_path
in
{files = [(driver_path, driver)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
@@ -509,7 +509,7 @@
Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
Path.implode driver_path ^ " -i" ^ Path.implode path
- val run_cmd = File.shell_path compiled_path
+ val run_cmd = File.bash_path compiled_path
in
{files = [(driver_path, driver)],
compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
@@ -551,12 +551,12 @@
val compile_cmd =
Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
- " -d " ^ File.shell_path path ^ " -classpath " ^ File.shell_path path ^ " " ^
- File.shell_path code_path ^ " " ^ File.shell_path driver_path
+ " -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.shell_path path ^ " Test"
+ " -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}
--- a/src/HOL/TPTP/atp_theory_export.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Mon Mar 07 21:09:28 2016 +0100
@@ -59,8 +59,8 @@
val exec = exec false
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
- File.shell_path (Path.explode path) ^ " " ^
- arguments ctxt false "" atp_timeout (File.shell_path prob_file)
+ File.bash_path (Path.explode path) ^ " " ^
+ arguments ctxt false "" atp_timeout (File.bash_path prob_file)
(ord, K [], K [])
val outcome =
Timeout.apply atp_timeout Isabelle_System.bash_output command
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Mar 07 21:09:28 2016 +0100
@@ -1028,8 +1028,8 @@
val outcome =
let
val code =
- Isabelle_System.bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
- \\"$KODKODI\"/bin/kodkodi" ^
+ Isabelle_System.bash ("cd " ^ File.bash_string temp_dir ^ ";\n\
+ \\"$KODKODI/bin/kodkodi\"" ^
(if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
(if max_solutions > 1 then " -solve-all" else "") ^
@@ -1038,9 +1038,9 @@
" -max-threads " ^ string_of_int max_threads
else
"") ^
- " < " ^ File.shell_path in_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path)
+ " < " ^ File.bash_path in_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path)
val (io_error, (ps, nontriv_js)) =
read_output_file out_path
||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Mar 07 21:09:28 2016 +0100
@@ -818,7 +818,7 @@
if getenv env_var = "" then
(warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
else
- (case Isabelle_System.bash_output (cmd ^ File.shell_path file) of
+ (case Isabelle_System.bash_output (cmd ^ File.bash_path file) of
(out, 0) => out
| (_, rc) =>
error ("Error caused by prolog system " ^ env_var ^
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Mar 07 21:09:28 2016 +0100
@@ -251,10 +251,10 @@
val _ = map (uncurry File.write) (includes @
[(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
(code_file, code), (main_file, main)])
- val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
+ val executable = File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
ghc_options ^ " " ^
- (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
+ (space_implode " " (map File.bash_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
" -o " ^ executable ^ ";"
val (_, compilation_time) =
elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Mar 07 21:09:28 2016 +0100
@@ -49,8 +49,8 @@
local
fun make_command command options problem_path proof_path =
- "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
- [File.shell_path problem_path, ")", ">", File.shell_path proof_path]
+ "(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
|> space_implode " "
fun with_trace ctxt msg f x =
@@ -79,7 +79,7 @@
Cache_IO.run_and_cache certs key mk_cmd input
| (SOME output, _) =>
with_trace ctxt ("Using cached certificate from " ^
- File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") I output))
+ Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
(* Z3 returns 1 if "get-model" or "get-model" fails *)
val normal_return_codes = [0, 1]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Mar 07 21:09:28 2016 +0100
@@ -283,10 +283,10 @@
val ord = effective_term_order ctxt name
val args =
- arguments ctxt full_proofs extra slice_timeout (File.shell_path prob_path)
+ arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path)
(ord, ord_info, sel_weights)
val command =
- "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
+ "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")"
|> enclose "TIMEFORMAT='%3R'; { time " " ; }"
val _ =
--- a/src/HOL/Tools/sat_solver.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Tools/sat_solver.ML Mon Mar 07 21:09:28 2016 +0100
@@ -633,7 +633,7 @@
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
- val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null"
+ val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " -t " ^ File.bash_path proofpath ^ "> /dev/null"
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm
fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -809,7 +809,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
+ val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " > /dev/null"
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -965,7 +965,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val cmd = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
+ val cmd = "\"$ZCHAFF_HOME/zchaff\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -991,8 +991,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val exec = getenv "BERKMIN_EXE"
- val cmd = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
+ val cmd = "\"$BERKMIN_HOME/${BERKMIN_EXE:-BerkMin561}\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
@@ -1018,7 +1017,7 @@
val serial_str = serial_string ()
val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
- val cmd = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
+ val cmd = "\"$JERUSAT_HOME/Jerusat1.3\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath
fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
fun readfn () = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
--- a/src/Pure/Concurrent/bash.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Pure/Concurrent/bash.ML Mon Mar 07 21:09:28 2016 +0100
@@ -38,10 +38,10 @@
val _ = getenv_strict "ISABELLE_BASH_PROCESS";
val status =
OS.Process.system
- ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.shell_path pid_path ^
- " bash " ^ File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path);
+ ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^
+ " bash " ^ File.bash_path script_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path);
val res =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => Result 0
--- a/src/Pure/Concurrent/bash_windows.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML Mon Mar 07 21:09:28 2016 +0100
@@ -36,9 +36,9 @@
let
val _ = File.write script_path script;
val bash_script =
- "bash " ^ File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path;
+ "bash " ^ File.bash_path script_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path;
val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
val rc =
Windows.simpleExecute ("",
--- a/src/Pure/General/file.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Pure/General/file.ML Mon Mar 07 21:09:28 2016 +0100
@@ -8,8 +8,9 @@
sig
val standard_path: Path.T -> string
val platform_path: Path.T -> string
- val shell_quote: string -> string
- val shell_path: Path.T -> string
+ val bash_string: string -> string
+ val bash_args: string list -> string
+ val bash_path: Path.T -> string
val cd: Path.T -> unit
val pwd: unit -> Path.T
val full_path: Path.T -> Path.T -> Path.T
@@ -47,8 +48,25 @@
val standard_path = Path.implode o Path.expand;
val platform_path = ML_System.platform_path o standard_path;
-val shell_quote = enclose "'" "'";
-val shell_path = shell_quote o standard_path;
+val bash_string =
+ translate_string (fn ch =>
+ let val c = ord ch in
+ (case ch of
+ "\t" => "$'\\t'"
+ | "\n" => "$'\\n'"
+ | "\f" => "$'\\f'"
+ | "\r" => "$'\\r'"
+ | _ =>
+ if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+ exists_string (fn c => c = ch) "-./:_" then ch
+ else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else "\\" ^ ch)
+ end);
+
+val bash_args = space_implode " " o map bash_string;
+
+val bash_path = bash_string o standard_path;
(* current working directory *)
--- a/src/Pure/System/isabelle_system.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Pure/System/isabelle_system.ML Mon Mar 07 21:09:28 2016 +0100
@@ -51,7 +51,7 @@
then SOME path
else NONE
end handle OS.SysErr _ => NONE) of
- SOME path => bash (File.shell_path path ^ " " ^ args)
+ SOME path => bash (File.bash_path path ^ " " ^ args)
| NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
fun system_command cmd =
@@ -64,7 +64,7 @@
fun mkdirs path =
if File.is_dir path then ()
else
- (bash ("perl -e \"use File::Path make_path; make_path(" ^ File.shell_path path ^ ");\"");
+ (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\"");
if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
fun mkdir path =
@@ -72,7 +72,7 @@
fun copy_dir src dst =
if File.eq (src, dst) then ()
- else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+ else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ());
fun copy_file src0 dst0 =
let
@@ -82,7 +82,7 @@
in
if File.eq (src, target) then ()
else
- ignore (system_command ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target))
+ ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target))
end;
fun copy_file_base (base_dir, src0) target_dir =
@@ -112,7 +112,7 @@
(* tmp dirs *)
-fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
fun with_tmp_dir name f =
let
--- a/src/Pure/Thy/present.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Pure/Thy/present.ML Mon Mar 07 21:09:28 2016 +0100
@@ -216,7 +216,7 @@
fun isabelle_document {verbose, purge} format name tags dir =
let
val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
- \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1";
+ \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
val _ = if verbose then writeln s else ();
val (out, rc) = Isabelle_System.bash_output s;
@@ -270,7 +270,7 @@
val _ = Isabelle_System.mkdirs doc_dir;
val _ =
Isabelle_System.isabelle_tool "latex"
- ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
+ ("-o sty " ^ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
val _ = write_tex_index tex_index doc_dir;
@@ -360,8 +360,8 @@
val _ = Isabelle_System.mkdirs doc_path;
val root_path = Path.append doc_path (Path.basic "root.tex");
val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
- val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
- val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
+ val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.bash_path root_path);
+ val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.bash_path root_path);
fun known name =
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
@@ -383,7 +383,7 @@
val _ = Isabelle_System.mkdirs target_dir;
val _ = Isabelle_System.copy_file result target;
in
- Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &")
+ Isabelle_System.isabelle_tool "display" (File.bash_path target ^ " &")
end);
end;
--- a/src/Tools/Code/code_target.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Tools/Code/code_target.ML Mon Mar 07 21:09:28 2016 +0100
@@ -385,7 +385,7 @@
generatedN args program all_public syms);
val cmd = make_command generatedN;
in
- if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+ if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
else ()
end;
--- a/src/Tools/cache_io.ML Mon Mar 07 20:44:47 2016 +0100
+++ b/src/Tools/cache_io.ML Mon Mar 07 21:09:28 2016 +0100
@@ -62,7 +62,7 @@
val table =
if File.exists cache_path then
let
- fun err () = error ("Cache IO: corrupted cache file: " ^ File.shell_path cache_path)
+ fun err () = error ("Cache IO: corrupted cache file: " ^ File.bash_path cache_path)
fun int_of_string s =
(case read_int (raw_explode s) of