common setup for system_out/system;
authorwenzelm
Thu Mar 06 20:17:50 2008 +0100 (2008-03-06)
changeset 26220d34b68c21f9a
parent 26219 2d026932f710
child 26221 e557c20158e2
common setup for system_out/system;
src/Pure/General/file.ML
src/Pure/General/secure.ML
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/system_shell.ML
     1.1 --- a/src/Pure/General/file.ML	Thu Mar 06 20:17:49 2008 +0100
     1.2 +++ b/src/Pure/General/file.ML	Thu Mar 06 20:17:50 2008 +0100
     1.3 @@ -98,8 +98,10 @@
     1.4        (case getenv "ISABELLE_FILE_IDENT" of
     1.5          "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
     1.6        | cmd =>
     1.7 -         let val id = execute ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path) in
     1.8 -           if id <> "" then id
     1.9 +         let
    1.10 +           val (id, rc) = system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path)
    1.11 +         in
    1.12 +           if id <> "" andalso rc = 0 then id
    1.13             else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
    1.14           end)));
    1.15  
     2.1 --- a/src/Pure/General/secure.ML	Thu Mar 06 20:17:49 2008 +0100
     2.2 +++ b/src/Pure/General/secure.ML	Thu Mar 06 20:17:50 2008 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4    val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
     2.5    val use: string -> unit
     2.6    val commit: unit -> unit
     2.7 -  val execute: string -> string
     2.8 +  val system_out: string -> string * int
     2.9    val system: string -> int
    2.10  end;
    2.11  
    2.12 @@ -57,11 +57,10 @@
    2.13  
    2.14  fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
    2.15  
    2.16 -val orig_execute = execute;
    2.17 -val orig_system = system;
    2.18 +val orig_system_out = system_out;
    2.19  
    2.20 -fun execute s = (secure_shell (); orig_execute s);
    2.21 -fun system s = (secure_shell (); orig_system s);
    2.22 +fun system_out s = (secure_shell (); orig_system_out s);
    2.23 +fun system s = #2 (system_out s);
    2.24  
    2.25  end;
    2.26  
    2.27 @@ -69,5 +68,5 @@
    2.28  val use_text = Secure.use_text;
    2.29  val use_file = Secure.use_file;
    2.30  fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
    2.31 -val execute = Secure.execute;
    2.32 +val system_out = Secure.system_out;
    2.33  val system = Secure.system;
     3.1 --- a/src/Pure/ML-Systems/alice.ML	Thu Mar 06 20:17:49 2008 +0100
     3.2 +++ b/src/Pure/ML-Systems/alice.ML	Thu Mar 06 20:17:50 2008 +0100
     3.3 @@ -11,6 +11,7 @@
     3.4  - use "ML-Systems/exn.ML";
     3.5  - use "ML-Systems/multithreading.ML";
     3.6  - use "ML-Systems/time_limit.ML";
     3.7 +- use "ML-Systems/system_shell.ML";
     3.8  - use "ML-Systems/alice.ML";
     3.9  - use "ROOT.ML";
    3.10  - Session.finish ();
    3.11 @@ -143,29 +144,9 @@
    3.12  
    3.13  (** OS related **)
    3.14  
    3.15 -(* current directory *)
    3.16 -
    3.17  val cd = OS.FileSys.chDir;
    3.18  val pwd = OS.FileSys.getDir;
    3.19  
    3.20 -
    3.21 -(* system command execution *)
    3.22 -
    3.23 -(*execute Unix command which doesn't take any input from stdin and
    3.24 -  sends its output to stdout; could be done more easily by Unix.execute,
    3.25 -  but that function doesn't use the PATH*)
    3.26 -fun execute command =
    3.27 -  let
    3.28 -    val tmp_name = OS.FileSys.tmpName ();
    3.29 -    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
    3.30 -    val result = TextIO.inputAll is;
    3.31 -  in
    3.32 -    TextIO.closeIn is;
    3.33 -    OS.FileSys.remove tmp_name;
    3.34 -    result
    3.35 -  end;
    3.36 -
    3.37 -(*plain version; with return code*)
    3.38  val system = OS.Process.system: string -> int;
    3.39  
    3.40  structure OS =
    3.41 @@ -182,9 +163,6 @@
    3.42    end;
    3.43  end;
    3.44  
    3.45 -
    3.46 -(* getenv *)
    3.47 -
    3.48  fun getenv var =
    3.49    (case OS.Process.getEnv var of
    3.50      NONE => ""
     4.1 --- a/src/Pure/ML-Systems/mosml.ML	Thu Mar 06 20:17:49 2008 +0100
     4.2 +++ b/src/Pure/ML-Systems/mosml.ML	Thu Mar 06 20:17:50 2008 +0100
     4.3 @@ -38,6 +38,7 @@
     4.4  use "ML-Systems/universal.ML";
     4.5  use "ML-Systems/multithreading.ML";
     4.6  use "ML-Systems/time_limit.ML";
     4.7 +use "ML-Systems/system_shell.ML";
     4.8  
     4.9  
    4.10  (*low-level pointer equality*)
    4.11 @@ -178,38 +179,11 @@
    4.12  
    4.13  (** OS related **)
    4.14  
    4.15 -(* current directory *)
    4.16 -
    4.17  val cd = OS.FileSys.chDir;
    4.18  val pwd = OS.FileSys.getDir;
    4.19  
    4.20 -
    4.21 -(* system command execution *)
    4.22 -
    4.23 -(*execute Unix command which doesn't take any input from stdin and
    4.24 -  sends its output to stdout; could be done more easily by Unix.execute,
    4.25 -  but that function doesn't use the PATH*)
    4.26 -fun execute command =
    4.27 -  let
    4.28 -    val tmp_name = FileSys.tmpName ();
    4.29 -    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
    4.30 -    val result = TextIO.inputAll is;
    4.31 -  in
    4.32 -    TextIO.closeIn is;
    4.33 -    FileSys.remove tmp_name;
    4.34 -    result
    4.35 -  end;
    4.36 -
    4.37 -(*plain version; with return code*)
    4.38 -fun system cmd =
    4.39 -  if Process.system cmd = Process.success then 0 else 1;
    4.40 -
    4.41 -
    4.42  val string_of_pid = Int.toString;
    4.43  
    4.44 -
    4.45 -(* getenv *)
    4.46 -
    4.47  fun getenv var =
    4.48    (case Process.getEnv var of
    4.49      NONE => ""
     5.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Thu Mar 06 20:17:49 2008 +0100
     5.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Mar 06 20:17:50 2008 +0100
     5.3 @@ -9,6 +9,8 @@
     5.4  else use "ML-Systems/universal.ML";
     5.5  use "ML-Systems/multithreading.ML";
     5.6  use "ML-Systems/time_limit.ML";
     5.7 +use "ML-Systems/system_shell.ML";
     5.8 +
     5.9  
    5.10  
    5.11  (** ML system and platform related **)
    5.12 @@ -190,27 +192,6 @@
    5.13  val pwd = OS.FileSys.getDir;
    5.14  
    5.15  
    5.16 -(* system command execution *)
    5.17 -
    5.18 -(*execute Unix command which doesn't take any input from stdin and
    5.19 -  sends its output to stdout; could be done more easily by Unix.execute,
    5.20 -  but that function doesn't use the PATH*)
    5.21 -fun execute command =
    5.22 -  let
    5.23 -    val tmp_name = OS.FileSys.tmpName ();
    5.24 -    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
    5.25 -    val result = TextIO.inputAll is;
    5.26 -  in
    5.27 -    TextIO.closeIn is;
    5.28 -    OS.FileSys.remove tmp_name;
    5.29 -    result
    5.30 -  end;
    5.31 -
    5.32 -(*plain version; with return code*)
    5.33 -fun system cmd =
    5.34 -  if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
    5.35 -
    5.36 -
    5.37  (*Convert a process ID to a decimal string (chiefly for tracing)*)
    5.38  fun string_of_pid pid =
    5.39    Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Mar 06 20:17:49 2008 +0100
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Mar 06 20:17:50 2008 +0100
     6.3 @@ -9,6 +9,7 @@
     6.4  use "ML-Systems/exn.ML";
     6.5  use "ML-Systems/universal.ML";
     6.6  use "ML-Systems/multithreading.ML";
     6.7 +use "ML-Systems/system_shell.ML";
     6.8  
     6.9  
    6.10  (*low-level pointer equality*)
    6.11 @@ -229,27 +230,12 @@
    6.12  
    6.13  (* system command execution *)
    6.14  
    6.15 -(*execute Unix command which doesn't take any input from stdin and
    6.16 -  sends its output to stdout; could be done more easily by Unix.execute,
    6.17 -  but that function doesn't use the PATH*)
    6.18 -fun execute command =
    6.19 -  let
    6.20 -    val tmp_name = OS.FileSys.tmpName ();
    6.21 -    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
    6.22 -    val result = TextIO.inputAll is;
    6.23 -  in
    6.24 -    TextIO.closeIn is;
    6.25 -    OS.FileSys.remove tmp_name;
    6.26 -    result
    6.27 -  end;
    6.28 -
    6.29 -(*plain version; with return code*)
    6.30 -val system = mk_int o OS.Process.system;
    6.31 +val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
    6.32  
    6.33  
    6.34  (*Convert a process ID to a decimal string (chiefly for tracing)*)
    6.35  fun string_of_pid pid =
    6.36 -    Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
    6.37 +  Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
    6.38  
    6.39  
    6.40  (* getenv *)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML-Systems/system_shell.ML	Thu Mar 06 20:17:50 2008 +0100
     7.3 @@ -0,0 +1,44 @@
     7.4 +(*  Title:      Pure/ML-Systems/system_shell.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Makarius
     7.7 +
     7.8 +Generic system shell processes (no provisions to propagate interrupts;
     7.9 +might still work via the controlling tty).
    7.10 +*)
    7.11 +
    7.12 +local
    7.13 +
    7.14 +fun read_file name =
    7.15 +  let val is = TextIO.openIn name
    7.16 +  in TextIO.inputAll is before TextIO.closeIn is end;
    7.17 +
    7.18 +fun write_file name txt =
    7.19 +  let val os = TextIO.openOut name
    7.20 +  in TextIO.output (os, txt) before TextIO.closeOut os end;
    7.21 +
    7.22 +in
    7.23 +
    7.24 +fun system_out script =
    7.25 +  let
    7.26 +    val script_name = OS.FileSys.tmpName ();
    7.27 +    val _ = write_file script_name script;
    7.28 +
    7.29 +    val output_name = OS.FileSys.tmpName ();
    7.30 +
    7.31 +    val status =
    7.32 +      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
    7.33 +        script_name ^ " /dev/null " ^ output_name);
    7.34 +    val rc =
    7.35 +      (case Posix.Process.fromStatus status of
    7.36 +        Posix.Process.W_EXITED => 0
    7.37 +      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    7.38 +      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    7.39 +      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    7.40 +
    7.41 +    val output = read_file output_name handle IO.Io _ => "";
    7.42 +    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    7.43 +    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    7.44 +  in (output, rc) end;
    7.45 +
    7.46 +end;
    7.47 +