renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Sat Feb 06 14:50:55 2010 +0100
@@ -54,10 +54,12 @@
(* call solver *)
val output_file = filename dir "sos_out"
- val (output, rv) = system_out (
- if File.exists cmd then space_implode " "
- [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
- else error ("Bad executable: " ^ File.platform_path cmd))
+ val (output, rv) =
+ bash_output
+ (if File.exists cmd then
+ space_implode " "
+ [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
+ else error ("Bad executable: " ^ File.platform_path cmd))
(* read and analyze output *)
val (res, res_msg) = find_failure rv
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Sat Feb 06 14:50:55 2010 +0100
@@ -1145,7 +1145,7 @@
val cplex_path = getenv "GLPK_PATH"
val cplex = if cplex_path = "" then "glpsol" else cplex_path
val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
- val answer = #1 (system_out command)
+ val answer = #1 (bash_output command)
in
let
val result = load_glpkResult resultname
@@ -1178,7 +1178,7 @@
val cplex = if cplex_path = "" then "cplex" else cplex_path
val _ = write_script scriptname lpname resultname
val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
- val answer = "return code "^(Int.toString (system command))
+ val answer = "return code "^(Int.toString (bash command))
in
let
val result = load_cplexResult resultname
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Sat Feb 06 14:50:55 2010 +0100
@@ -40,7 +40,7 @@
val pmu =
if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
else eindhoven_home ^ "/pmu";
- in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
+ in #1 (bash_output ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
in
fn cgoal =>
let
--- a/src/HOL/Modelcheck/mucke_oracle.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Sat Feb 06 14:50:55 2010 +0100
@@ -498,7 +498,7 @@
else mucke_home ^ "/mucke";
val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
val _ = File.write mucke_input_file s;
- val (result, _) = system_out (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
+ val (result, _) = bash_output (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
in
if not (!trace_mc) then (File.rm mucke_input_file) else ();
result
--- a/src/HOL/SMT/Tools/smt_solver.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML Sat Feb 06 14:50:55 2010 +0100
@@ -156,7 +156,7 @@
else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
val _ = tracing msg
in
- system_out (space_implode " " ("perl -w" ::
+ bash_output (space_implode " " ("perl -w" ::
File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
map File.shell_quote (solver @ args) @
map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sat Feb 06 14:50:55 2010 +0100
@@ -168,7 +168,7 @@
fun run_on probfile =
if File.exists cmd then
write probfile clauses
- |> pair (apfst split_time' (system_out (cmd_line probfile)))
+ |> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd);
(* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
@@ -306,7 +306,7 @@
fun get_systems () =
let
- val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+ val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
in
if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
else split_lines answer
--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Feb 06 14:50:55 2010 +0100
@@ -1004,7 +1004,7 @@
read_next_problems (Substring.full (File.read path), [], []) |>> rev ||> rev
(* The fudge term below is to account for Kodkodi's slow start-up time, which
- is partly due to the JVM and partly due to the ML "system" function. *)
+ is partly due to the JVM and partly due to the ML "bash" function. *)
val fudge_ms = 250
(* bool -> Time.time option -> int -> int -> problem list -> outcome *)
@@ -1053,7 +1053,7 @@
val outcome =
let
val code =
- system ("cd " ^ temp_dir ^ ";\n" ^
+ bash ("cd " ^ temp_dir ^ ";\n" ^
"env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
\JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
\$JAVA_LIBRARY_PATH\" \
--- a/src/HOL/Tools/sat_solver.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/Tools/sat_solver.ML Sat Feb 06 14:50:55 2010 +0100
@@ -282,7 +282,7 @@
(* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
fun make_external_solver cmd writefn readfn fm =
- (writefn fm; system cmd; readfn ());
+ (writefn fm; bash cmd; readfn ());
(* ------------------------------------------------------------------------- *)
(* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
--- a/src/HOL/ex/svc_funcs.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Sat Feb 06 14:50:55 2010 +0100
@@ -62,11 +62,11 @@
val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
val svc_input_file = File.tmp_path (Path.basic "SVM_in");
val svc_output_file = File.tmp_path (Path.basic "SVM_out");
- val _ = (File.write svc_input_file svc_input;
- #1 (system_out (check_valid ^ " -dump-result " ^
- File.shell_path svc_output_file ^
- " " ^ File.shell_path svc_input_file ^
- ">/dev/null 2>&1")))
+ val _ = File.write svc_input_file svc_input;
+ val _ =
+ bash_output (check_valid ^ " -dump-result " ^
+ File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
+ ">/dev/null 2>&1")
val svc_output =
(case try File.read svc_output_file of
SOME out => out
--- a/src/Pure/General/file.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/General/file.ML Sat Feb 06 14:50:55 2010 +0100
@@ -14,7 +14,6 @@
val full_path: Path.T -> Path.T
val tmp_path: Path.T -> Path.T
val isabelle_tool: string -> string -> int
- val system_command: string -> unit
eqtype ident
val rep_ident: ident -> string
val ident: Path.T -> ident option
@@ -75,11 +74,11 @@
then SOME path
else NONE
end handle OS.SysErr _ => NONE) of
- SOME path => system (shell_quote path ^ " " ^ args)
+ SOME path => bash (shell_quote path ^ " " ^ args)
| NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
fun system_command cmd =
- if system cmd <> 0 then error ("System command failed: " ^ cmd)
+ if bash cmd <> 0 then error ("System command failed: " ^ cmd)
else ();
@@ -116,7 +115,7 @@
SOME id => id
| NONE =>
let val (id, rc) = (*potentially slow*)
- system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
+ bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
in
if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
--- a/src/Pure/General/secure.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/General/secure.ML Sat Feb 06 14:50:55 2010 +0100
@@ -15,8 +15,8 @@
val toplevel_pp: string list -> string -> unit
val open_unsynchronized: unit -> unit
val commit: unit -> unit
- val system_out: string -> string * int
- val system: string -> int
+ val bash_output: string -> string * int
+ val bash: string -> int
end;
structure Secure: SECURE =
@@ -61,12 +61,12 @@
fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
-val orig_system_out = system_out;
+val orig_bash_output = bash_output;
-fun system_out s = (secure_shell (); orig_system_out s);
+fun bash_output s = (secure_shell (); orig_bash_output s);
-fun system s =
- (case system_out s of
+fun bash s =
+ (case bash_output s of
("", rc) => rc
| (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
@@ -78,5 +78,5 @@
fun use s = Secure.use_file ML_Parse.global_context true s
handle ERROR msg => (writeln msg; error "ML error");
val toplevel_pp = Secure.toplevel_pp;
-val system_out = Secure.system_out;
-val system = Secure.system;
+val bash_output = Secure.bash_output;
+val bash = Secure.bash;
--- a/src/Pure/IsaMakefile Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/IsaMakefile Sat Feb 06 14:50:55 2010 +0100
@@ -21,19 +21,18 @@
## Pure
-BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML \
+BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML \
ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \
- ML-Systems/ml_name_space.ML \
- ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
- ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
- ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \
- ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \
- ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \
- ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
- ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
- ML-Systems/timing.ML ML-Systems/time_limit.ML \
- ML-Systems/universal.ML ML-Systems/unsynchronized.ML
+ ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML \
+ ML-Systems/mosml.ML ML-Systems/multithreading.ML \
+ ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
+ ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml-5.2.ML ML-Systems/polyml-5.2.1.ML \
+ ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
+ ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/thread_dummy.ML ML-Systems/timing.ML \
+ ML-Systems/time_limit.ML ML-Systems/universal.ML \
+ ML-Systems/unsynchronized.ML
RAW: $(OUT)/RAW
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/bash.ML Sat Feb 06 14:50:55 2010 +0100
@@ -0,0 +1,43 @@
+(* Title: Pure/ML-Systems/bash.ML
+ Author: Makarius
+
+Generic GNU bash processes (no provisions to propagate interrupts, but
+could work via the controlling tty).
+*)
+
+local
+
+fun read_file name =
+ let val is = TextIO.openIn name
+ in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
+
+fun write_file name txt =
+ let val os = TextIO.openOut name
+ in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
+
+in
+
+fun bash_output script =
+ let
+ val script_name = OS.FileSys.tmpName ();
+ val _ = write_file script_name script;
+
+ val output_name = OS.FileSys.tmpName ();
+
+ val status =
+ OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
+ script_name ^ " /dev/null " ^ output_name);
+ val rc =
+ (case Posix.Process.fromStatus status of
+ Posix.Process.W_EXITED => 0
+ | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+ | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+ | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+ val output = read_file output_name handle IO.Io _ => "";
+ val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
+ val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
+ in (output, rc) end;
+
+end;
+
--- a/src/Pure/ML-Systems/mosml.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Sat Feb 06 14:50:55 2010 +0100
@@ -229,7 +229,7 @@
in
-fun system_out script =
+fun bash_output script =
let
val script_name = OS.FileSys.tmpName ();
val _ = write_file script_name script;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Feb 06 14:50:55 2010 +0100
@@ -8,7 +8,7 @@
sig
val interruptible: ('a -> 'b) -> 'a -> 'b
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
- val system_out: string -> string * int
+ val bash_output: string -> string * int
structure TimeLimit: TIME_LIMIT
end;
@@ -156,9 +156,9 @@
end;
-(* system shell processes, with propagation of interrupts *)
+(* GNU bash processes, with propagation of interrupts *)
-fun system_out script = with_attributes no_interrupts (fn orig_atts =>
+fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
let
val script_name = OS.FileSys.tmpName ();
val _ = write_file script_name script;
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Sat Feb 06 14:50:55 2010 +0100
@@ -9,7 +9,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/timing.ML";
-use "ML-Systems/system_shell.ML";
+use "ML-Systems/bash.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
--- a/src/Pure/ML-Systems/smlnj.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Feb 06 14:50:55 2010 +0100
@@ -14,7 +14,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/timing.ML";
-use "ML-Systems/system_shell.ML";
+use "ML-Systems/bash.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
@@ -179,7 +179,7 @@
(* system command execution *)
-val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
+val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
fun process_id pid =
Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
--- a/src/Pure/ML-Systems/system_shell.ML Sat Feb 06 14:39:33 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: Pure/ML-Systems/system_shell.ML
- Author: Makarius
-
-Generic system shell processes (no provisions to propagate interrupts;
-might still work via the controlling tty).
-*)
-
-local
-
-fun read_file name =
- let val is = TextIO.openIn name
- in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
- let val os = TextIO.openOut name
- in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
-fun system_out script =
- let
- val script_name = OS.FileSys.tmpName ();
- val _ = write_file script_name script;
-
- val output_name = OS.FileSys.tmpName ();
-
- val status =
- OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
- script_name ^ " /dev/null " ^ output_name);
- val rc =
- (case Posix.Process.fromStatus status of
- Posix.Process.W_EXITED => 0
- | Posix.Process.W_EXITSTATUS w => Word8.toInt w
- | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
- | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
-
- val output = read_file output_name handle IO.Io _ => "";
- val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
- val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
- in (output, rc) end;
-
-end;
-
--- a/src/Pure/System/isabelle_system.scala Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Feb 06 14:50:55 2010 +0100
@@ -162,7 +162,7 @@
/** system tools **/
- def system_out(script: String): (String, Int) =
+ def bash_output(script: String): (String, Int) =
{
Standard_System.with_tmp_file("isabelle_script") { script_file =>
Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
--- a/src/Pure/Thy/present.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/Thy/present.ML Sat Feb 06 14:50:55 2010 +0100
@@ -328,7 +328,7 @@
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
val doc_path = Path.append result_path (Path.ext format (Path.basic name));
val _ = if verbose then writeln s else ();
- val (out, rc) = system_out s;
+ val (out, rc) = bash_output s;
val _ =
if not (File.exists doc_path) orelse rc <> 0 then
cat_error out ("Failed to build document " ^ quote (show_path doc_path))
--- a/src/Tools/Compute_Oracle/am_ghc.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Tools/Compute_Oracle/am_ghc.ML Sat Feb 06 14:50:55 2010 +0100
@@ -228,7 +228,7 @@
val module_file = tmp_file (module^".hs")
val object_file = tmp_file (module^".o")
val _ = writeTextFile module_file source
- val _ = system ((!ghc)^" -c "^module_file)
+ val _ = bash ((!ghc)^" -c "^module_file)
val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
in
(guid, module_file, arity)
@@ -309,7 +309,7 @@
val term = print_term arity_of 0 t
val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
val _ = writeTextFile call_file call_source
- val _ = system ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
+ val _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
val t' = parse_result arity_of result
val _ = OS.FileSys.remove call_file