renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
authorwenzelm
Sat Feb 06 14:50:55 2010 +0100 (2010-02-06)
changeset 35010d6e492cea6e4
parent 35009 5408e5207131
child 35011 9e55e87434ff
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/SMT/Tools/smt_solver.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/svc_funcs.ML
src/Pure/General/file.ML
src/Pure/General/secure.ML
src/Pure/IsaMakefile
src/Pure/ML-Systems/bash.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/system_shell.ML
src/Pure/System/isabelle_system.scala
src/Pure/Thy/present.ML
src/Tools/Compute_Oracle/am_ghc.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Sat Feb 06 14:39:33 2010 +0100
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Sat Feb 06 14:50:55 2010 +0100
     1.3 @@ -54,10 +54,12 @@
     1.4  
     1.5      (* call solver *)
     1.6      val output_file = filename dir "sos_out"
     1.7 -    val (output, rv) = system_out (
     1.8 -      if File.exists cmd then space_implode " "
     1.9 -        [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
    1.10 -      else error ("Bad executable: " ^ File.platform_path cmd))
    1.11 +    val (output, rv) =
    1.12 +      bash_output
    1.13 +       (if File.exists cmd then
    1.14 +          space_implode " "
    1.15 +            [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
    1.16 +        else error ("Bad executable: " ^ File.platform_path cmd))
    1.17  
    1.18      (* read and analyze output *)
    1.19      val (res, res_msg) = find_failure rv
     2.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Sat Feb 06 14:39:33 2010 +0100
     2.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Sat Feb 06 14:50:55 2010 +0100
     2.3 @@ -1145,7 +1145,7 @@
     2.4      val cplex_path = getenv "GLPK_PATH"
     2.5      val cplex = if cplex_path = "" then "glpsol" else cplex_path
     2.6      val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
     2.7 -    val answer = #1 (system_out command)
     2.8 +    val answer = #1 (bash_output command)
     2.9      in
    2.10      let
    2.11          val result = load_glpkResult resultname
    2.12 @@ -1178,7 +1178,7 @@
    2.13      val cplex = if cplex_path = "" then "cplex" else cplex_path
    2.14      val _ = write_script scriptname lpname resultname
    2.15      val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
    2.16 -    val answer = "return code "^(Int.toString (system command))
    2.17 +    val answer = "return code "^(Int.toString (bash command))
    2.18      in
    2.19      let
    2.20          val result = load_cplexResult resultname
     3.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Sat Feb 06 14:39:33 2010 +0100
     3.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Sat Feb 06 14:50:55 2010 +0100
     3.3 @@ -40,7 +40,7 @@
     3.4        val pmu =
     3.5          if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
     3.6          else eindhoven_home ^ "/pmu";
     3.7 -    in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
     3.8 +    in #1 (bash_output ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
     3.9  in
    3.10    fn cgoal =>
    3.11      let
     4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Sat Feb 06 14:39:33 2010 +0100
     4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sat Feb 06 14:50:55 2010 +0100
     4.3 @@ -498,7 +498,7 @@
     4.4        else mucke_home ^ "/mucke";
     4.5      val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
     4.6      val _ = File.write mucke_input_file s;
     4.7 -    val (result, _) = system_out (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
     4.8 +    val (result, _) = bash_output (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
     4.9    in
    4.10      if not (!trace_mc) then (File.rm mucke_input_file) else (); 
    4.11      result
     5.1 --- a/src/HOL/SMT/Tools/smt_solver.ML	Sat Feb 06 14:39:33 2010 +0100
     5.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML	Sat Feb 06 14:50:55 2010 +0100
     5.3 @@ -156,7 +156,7 @@
     5.4        else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
     5.5      val _ = tracing msg
     5.6    in
     5.7 -    system_out (space_implode " " ("perl -w" ::
     5.8 +    bash_output (space_implode " " ("perl -w" ::
     5.9        File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
    5.10        map File.shell_quote (solver @ args) @
    5.11        map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
     6.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Feb 06 14:39:33 2010 +0100
     6.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Feb 06 14:50:55 2010 +0100
     6.3 @@ -168,7 +168,7 @@
     6.4      fun run_on probfile =
     6.5        if File.exists cmd then
     6.6          write probfile clauses
     6.7 -        |> pair (apfst split_time' (system_out (cmd_line probfile)))
     6.8 +        |> pair (apfst split_time' (bash_output (cmd_line probfile)))
     6.9        else error ("Bad executable: " ^ Path.implode cmd);
    6.10  
    6.11      (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
    6.12 @@ -306,7 +306,7 @@
    6.13  
    6.14  fun get_systems () =
    6.15    let
    6.16 -    val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
    6.17 +    val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
    6.18    in
    6.19      if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
    6.20      else split_lines answer
     7.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Feb 06 14:39:33 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Feb 06 14:50:55 2010 +0100
     7.3 @@ -1004,7 +1004,7 @@
     7.4    read_next_problems (Substring.full (File.read path), [], []) |>> rev ||> rev
     7.5  
     7.6  (* The fudge term below is to account for Kodkodi's slow start-up time, which
     7.7 -   is partly due to the JVM and partly due to the ML "system" function. *)
     7.8 +   is partly due to the JVM and partly due to the ML "bash" function. *)
     7.9  val fudge_ms = 250
    7.10  
    7.11  (* bool -> Time.time option -> int -> int -> problem list -> outcome *)
    7.12 @@ -1053,7 +1053,7 @@
    7.13            val outcome =
    7.14              let
    7.15                val code =
    7.16 -                system ("cd " ^ temp_dir ^ ";\n" ^
    7.17 +                bash ("cd " ^ temp_dir ^ ";\n" ^
    7.18                          "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
    7.19                          \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
    7.20                          \$JAVA_LIBRARY_PATH\" \
     8.1 --- a/src/HOL/Tools/sat_solver.ML	Sat Feb 06 14:39:33 2010 +0100
     8.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Feb 06 14:50:55 2010 +0100
     8.3 @@ -282,7 +282,7 @@
     8.4    (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
     8.5  
     8.6    fun make_external_solver cmd writefn readfn fm =
     8.7 -    (writefn fm; system cmd; readfn ());
     8.8 +    (writefn fm; bash cmd; readfn ());
     8.9  
    8.10  (* ------------------------------------------------------------------------- *)
    8.11  (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
     9.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Feb 06 14:39:33 2010 +0100
     9.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Feb 06 14:50:55 2010 +0100
     9.3 @@ -62,11 +62,11 @@
     9.4        val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
     9.5        val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
     9.6        val svc_output_file = File.tmp_path (Path.basic "SVM_out");
     9.7 -      val _ = (File.write svc_input_file svc_input;
     9.8 -               #1 (system_out (check_valid ^ " -dump-result " ^
     9.9 -                        File.shell_path svc_output_file ^
    9.10 -                        " " ^ File.shell_path svc_input_file ^
    9.11 -                        ">/dev/null 2>&1")))
    9.12 +      val _ = File.write svc_input_file svc_input;
    9.13 +      val _ =
    9.14 +        bash_output (check_valid ^ " -dump-result " ^
    9.15 +          File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
    9.16 +          ">/dev/null 2>&1")
    9.17        val svc_output =
    9.18          (case try File.read svc_output_file of
    9.19            SOME out => out
    10.1 --- a/src/Pure/General/file.ML	Sat Feb 06 14:39:33 2010 +0100
    10.2 +++ b/src/Pure/General/file.ML	Sat Feb 06 14:50:55 2010 +0100
    10.3 @@ -14,7 +14,6 @@
    10.4    val full_path: Path.T -> Path.T
    10.5    val tmp_path: Path.T -> Path.T
    10.6    val isabelle_tool: string -> string -> int
    10.7 -  val system_command: string -> unit
    10.8    eqtype ident
    10.9    val rep_ident: ident -> string
   10.10    val ident: Path.T -> ident option
   10.11 @@ -75,11 +74,11 @@
   10.12          then SOME path
   10.13          else NONE
   10.14        end handle OS.SysErr _ => NONE) of
   10.15 -    SOME path => system (shell_quote path ^ " " ^ args)
   10.16 +    SOME path => bash (shell_quote path ^ " " ^ args)
   10.17    | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
   10.18  
   10.19  fun system_command cmd =
   10.20 -  if system cmd <> 0 then error ("System command failed: " ^ cmd)
   10.21 +  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
   10.22    else ();
   10.23  
   10.24  
   10.25 @@ -116,7 +115,7 @@
   10.26                SOME id => id
   10.27              | NONE =>
   10.28                  let val (id, rc) =  (*potentially slow*)
   10.29 -                  system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
   10.30 +                  bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
   10.31                  in
   10.32                    if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
   10.33                    else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
    11.1 --- a/src/Pure/General/secure.ML	Sat Feb 06 14:39:33 2010 +0100
    11.2 +++ b/src/Pure/General/secure.ML	Sat Feb 06 14:50:55 2010 +0100
    11.3 @@ -15,8 +15,8 @@
    11.4    val toplevel_pp: string list -> string -> unit
    11.5    val open_unsynchronized: unit -> unit
    11.6    val commit: unit -> unit
    11.7 -  val system_out: string -> string * int
    11.8 -  val system: string -> int
    11.9 +  val bash_output: string -> string * int
   11.10 +  val bash: string -> int
   11.11  end;
   11.12  
   11.13  structure Secure: SECURE =
   11.14 @@ -61,12 +61,12 @@
   11.15  
   11.16  fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
   11.17  
   11.18 -val orig_system_out = system_out;
   11.19 +val orig_bash_output = bash_output;
   11.20  
   11.21 -fun system_out s = (secure_shell (); orig_system_out s);
   11.22 +fun bash_output s = (secure_shell (); orig_bash_output s);
   11.23  
   11.24 -fun system s =
   11.25 -  (case system_out s of
   11.26 +fun bash s =
   11.27 +  (case bash_output s of
   11.28      ("", rc) => rc
   11.29    | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
   11.30  
   11.31 @@ -78,5 +78,5 @@
   11.32  fun use s = Secure.use_file ML_Parse.global_context true s
   11.33    handle ERROR msg => (writeln msg; error "ML error");
   11.34  val toplevel_pp = Secure.toplevel_pp;
   11.35 -val system_out = Secure.system_out;
   11.36 -val system = Secure.system;
   11.37 +val bash_output = Secure.bash_output;
   11.38 +val bash = Secure.bash;
    12.1 --- a/src/Pure/IsaMakefile	Sat Feb 06 14:39:33 2010 +0100
    12.2 +++ b/src/Pure/IsaMakefile	Sat Feb 06 14:50:55 2010 +0100
    12.3 @@ -21,19 +21,18 @@
    12.4  
    12.5  ## Pure
    12.6  
    12.7 -BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML			\
    12.8 +BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML	\
    12.9    ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML	\
   12.10 -  ML-Systems/ml_name_space.ML				\
   12.11 -  ML-Systems/ml_pretty.ML ML-Systems/mosml.ML				\
   12.12 -  ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
   12.13 -  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML		\
   12.14 -  ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML			\
   12.15 -  ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML			\
   12.16 -  ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML			\
   12.17 -  ML-Systems/proper_int.ML ML-Systems/smlnj.ML				\
   12.18 -  ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
   12.19 -  ML-Systems/timing.ML ML-Systems/time_limit.ML				\
   12.20 -  ML-Systems/universal.ML ML-Systems/unsynchronized.ML
   12.21 +  ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML			\
   12.22 +  ML-Systems/mosml.ML ML-Systems/multithreading.ML			\
   12.23 +  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
   12.24 +  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
   12.25 +  ML-Systems/polyml-5.2.ML ML-Systems/polyml-5.2.1.ML			\
   12.26 +  ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
   12.27 +  ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
   12.28 +  ML-Systems/thread_dummy.ML ML-Systems/timing.ML			\
   12.29 +  ML-Systems/time_limit.ML ML-Systems/universal.ML			\
   12.30 +  ML-Systems/unsynchronized.ML
   12.31  
   12.32  RAW: $(OUT)/RAW
   12.33  
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Pure/ML-Systems/bash.ML	Sat Feb 06 14:50:55 2010 +0100
    13.3 @@ -0,0 +1,43 @@
    13.4 +(*  Title:      Pure/ML-Systems/bash.ML
    13.5 +    Author:     Makarius
    13.6 +
    13.7 +Generic GNU bash processes (no provisions to propagate interrupts, but
    13.8 +could work via the controlling tty).
    13.9 +*)
   13.10 +
   13.11 +local
   13.12 +
   13.13 +fun read_file name =
   13.14 +  let val is = TextIO.openIn name
   13.15 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
   13.16 +
   13.17 +fun write_file name txt =
   13.18 +  let val os = TextIO.openOut name
   13.19 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
   13.20 +
   13.21 +in
   13.22 +
   13.23 +fun bash_output script =
   13.24 +  let
   13.25 +    val script_name = OS.FileSys.tmpName ();
   13.26 +    val _ = write_file script_name script;
   13.27 +
   13.28 +    val output_name = OS.FileSys.tmpName ();
   13.29 +
   13.30 +    val status =
   13.31 +      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
   13.32 +        script_name ^ " /dev/null " ^ output_name);
   13.33 +    val rc =
   13.34 +      (case Posix.Process.fromStatus status of
   13.35 +        Posix.Process.W_EXITED => 0
   13.36 +      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
   13.37 +      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
   13.38 +      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
   13.39 +
   13.40 +    val output = read_file output_name handle IO.Io _ => "";
   13.41 +    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
   13.42 +    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   13.43 +  in (output, rc) end;
   13.44 +
   13.45 +end;
   13.46 +
    14.1 --- a/src/Pure/ML-Systems/mosml.ML	Sat Feb 06 14:39:33 2010 +0100
    14.2 +++ b/src/Pure/ML-Systems/mosml.ML	Sat Feb 06 14:50:55 2010 +0100
    14.3 @@ -229,7 +229,7 @@
    14.4  
    14.5  in
    14.6  
    14.7 -fun system_out script =
    14.8 +fun bash_output script =
    14.9    let
   14.10      val script_name = OS.FileSys.tmpName ();
   14.11      val _ = write_file script_name script;
    15.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:39:33 2010 +0100
    15.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:50:55 2010 +0100
    15.3 @@ -8,7 +8,7 @@
    15.4  sig
    15.5    val interruptible: ('a -> 'b) -> 'a -> 'b
    15.6    val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    15.7 -  val system_out: string -> string * int
    15.8 +  val bash_output: string -> string * int
    15.9    structure TimeLimit: TIME_LIMIT
   15.10  end;
   15.11  
   15.12 @@ -156,9 +156,9 @@
   15.13  end;
   15.14  
   15.15  
   15.16 -(* system shell processes, with propagation of interrupts *)
   15.17 +(* GNU bash processes, with propagation of interrupts *)
   15.18  
   15.19 -fun system_out script = with_attributes no_interrupts (fn orig_atts =>
   15.20 +fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
   15.21    let
   15.22      val script_name = OS.FileSys.tmpName ();
   15.23      val _ = write_file script_name script;
    16.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 06 14:39:33 2010 +0100
    16.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Feb 06 14:50:55 2010 +0100
    16.3 @@ -9,7 +9,7 @@
    16.4  use "ML-Systems/multithreading.ML";
    16.5  use "ML-Systems/time_limit.ML";
    16.6  use "ML-Systems/timing.ML";
    16.7 -use "ML-Systems/system_shell.ML";
    16.8 +use "ML-Systems/bash.ML";
    16.9  use "ML-Systems/ml_pretty.ML";
   16.10  use "ML-Systems/use_context.ML";
   16.11  
    17.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Feb 06 14:39:33 2010 +0100
    17.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Feb 06 14:50:55 2010 +0100
    17.3 @@ -14,7 +14,7 @@
    17.4  use "ML-Systems/thread_dummy.ML";
    17.5  use "ML-Systems/multithreading.ML";
    17.6  use "ML-Systems/timing.ML";
    17.7 -use "ML-Systems/system_shell.ML";
    17.8 +use "ML-Systems/bash.ML";
    17.9  use "ML-Systems/ml_name_space.ML";
   17.10  use "ML-Systems/ml_pretty.ML";
   17.11  use "ML-Systems/use_context.ML";
   17.12 @@ -179,7 +179,7 @@
   17.13  
   17.14  (* system command execution *)
   17.15  
   17.16 -val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
   17.17 +val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
   17.18  
   17.19  fun process_id pid =
   17.20    Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
    18.1 --- a/src/Pure/ML-Systems/system_shell.ML	Sat Feb 06 14:39:33 2010 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,43 +0,0 @@
    18.4 -(*  Title:      Pure/ML-Systems/system_shell.ML
    18.5 -    Author:     Makarius
    18.6 -
    18.7 -Generic system shell processes (no provisions to propagate interrupts;
    18.8 -might still work via the controlling tty).
    18.9 -*)
   18.10 -
   18.11 -local
   18.12 -
   18.13 -fun read_file name =
   18.14 -  let val is = TextIO.openIn name
   18.15 -  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
   18.16 -
   18.17 -fun write_file name txt =
   18.18 -  let val os = TextIO.openOut name
   18.19 -  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
   18.20 -
   18.21 -in
   18.22 -
   18.23 -fun system_out script =
   18.24 -  let
   18.25 -    val script_name = OS.FileSys.tmpName ();
   18.26 -    val _ = write_file script_name script;
   18.27 -
   18.28 -    val output_name = OS.FileSys.tmpName ();
   18.29 -
   18.30 -    val status =
   18.31 -      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
   18.32 -        script_name ^ " /dev/null " ^ output_name);
   18.33 -    val rc =
   18.34 -      (case Posix.Process.fromStatus status of
   18.35 -        Posix.Process.W_EXITED => 0
   18.36 -      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
   18.37 -      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
   18.38 -      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
   18.39 -
   18.40 -    val output = read_file output_name handle IO.Io _ => "";
   18.41 -    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
   18.42 -    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   18.43 -  in (output, rc) end;
   18.44 -
   18.45 -end;
   18.46 -
    19.1 --- a/src/Pure/System/isabelle_system.scala	Sat Feb 06 14:39:33 2010 +0100
    19.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Feb 06 14:50:55 2010 +0100
    19.3 @@ -162,7 +162,7 @@
    19.4  
    19.5    /** system tools **/
    19.6  
    19.7 -  def system_out(script: String): (String, Int) =
    19.8 +  def bash_output(script: String): (String, Int) =
    19.9    {
   19.10      Standard_System.with_tmp_file("isabelle_script") { script_file =>
   19.11        Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
    20.1 --- a/src/Pure/Thy/present.ML	Sat Feb 06 14:39:33 2010 +0100
    20.2 +++ b/src/Pure/Thy/present.ML	Sat Feb 06 14:50:55 2010 +0100
    20.3 @@ -328,7 +328,7 @@
    20.4        \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
    20.5      val doc_path = Path.append result_path (Path.ext format (Path.basic name));
    20.6      val _ = if verbose then writeln s else ();
    20.7 -    val (out, rc) = system_out s;
    20.8 +    val (out, rc) = bash_output s;
    20.9      val _ =
   20.10        if not (File.exists doc_path) orelse rc <> 0 then
   20.11          cat_error out ("Failed to build document " ^ quote (show_path doc_path))
    21.1 --- a/src/Tools/Compute_Oracle/am_ghc.ML	Sat Feb 06 14:39:33 2010 +0100
    21.2 +++ b/src/Tools/Compute_Oracle/am_ghc.ML	Sat Feb 06 14:50:55 2010 +0100
    21.3 @@ -228,7 +228,7 @@
    21.4          val module_file = tmp_file (module^".hs")
    21.5          val object_file = tmp_file (module^".o")
    21.6          val _ = writeTextFile module_file source
    21.7 -        val _ = system ((!ghc)^" -c "^module_file)
    21.8 +        val _ = bash ((!ghc)^" -c "^module_file)
    21.9          val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
   21.10      in
   21.11          (guid, module_file, arity)      
   21.12 @@ -309,7 +309,7 @@
   21.13          val term = print_term arity_of 0 t
   21.14          val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
   21.15          val _ = writeTextFile call_file call_source
   21.16 -        val _ = system ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
   21.17 +        val _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
   21.18          val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
   21.19          val t' = parse_result arity_of result
   21.20          val _ = OS.FileSys.remove call_file