# HG changeset patch # User wenzelm # Date 1457381368 -3600 # Node ID 9498623b27f05d664c379ea98b530efdf8be5865 # Parent f8ebb715e06d3a77a19b232a1b72eacec695b84a 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; diff -r f8ebb715e06d -r 9498623b27f0 NEWS --- 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. diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Library/Old_SMT/old_smt_solver.ML --- 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 = diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- 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 "" diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Library/code_test.ML --- 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} diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/TPTP/atp_theory_export.ML --- 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 diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Tools/Nitpick/kodkod.ML --- 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) diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 ^ diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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) diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Tools/SMT/smt_solver.ML --- 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] diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 _ = diff -r f8ebb715e06d -r 9498623b27f0 src/HOL/Tools/sat_solver.ML --- 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 () diff -r f8ebb715e06d -r 9498623b27f0 src/Pure/Concurrent/bash.ML --- 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 diff -r f8ebb715e06d -r 9498623b27f0 src/Pure/Concurrent/bash_windows.ML --- 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 ("", diff -r f8ebb715e06d -r 9498623b27f0 src/Pure/General/file.ML --- 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 *) diff -r f8ebb715e06d -r 9498623b27f0 src/Pure/System/isabelle_system.ML --- 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 diff -r f8ebb715e06d -r 9498623b27f0 src/Pure/Thy/present.ML --- 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; diff -r f8ebb715e06d -r 9498623b27f0 src/Tools/Code/code_target.ML --- 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; diff -r f8ebb715e06d -r 9498623b27f0 src/Tools/cache_io.ML --- 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