src/Pure/ML-Systems/system_shell.ML
changeset 26220 d34b68c21f9a
child 26504 6e87c0a60104
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/system_shell.ML	Thu Mar 06 20:17:50 2008 +0100
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  Title:      Pure/ML-Systems/system_shell.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Generic system shell processes (no provisions to propagate interrupts;
     1.9 +might still work via the controlling tty).
    1.10 +*)
    1.11 +
    1.12 +local
    1.13 +
    1.14 +fun read_file name =
    1.15 +  let val is = TextIO.openIn name
    1.16 +  in TextIO.inputAll is before TextIO.closeIn is end;
    1.17 +
    1.18 +fun write_file name txt =
    1.19 +  let val os = TextIO.openOut name
    1.20 +  in TextIO.output (os, txt) before TextIO.closeOut os end;
    1.21 +
    1.22 +in
    1.23 +
    1.24 +fun system_out script =
    1.25 +  let
    1.26 +    val script_name = OS.FileSys.tmpName ();
    1.27 +    val _ = write_file script_name script;
    1.28 +
    1.29 +    val output_name = OS.FileSys.tmpName ();
    1.30 +
    1.31 +    val status =
    1.32 +      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
    1.33 +        script_name ^ " /dev/null " ^ output_name);
    1.34 +    val rc =
    1.35 +      (case Posix.Process.fromStatus status of
    1.36 +        Posix.Process.W_EXITED => 0
    1.37 +      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    1.38 +      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    1.39 +      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    1.40 +
    1.41 +    val output = read_file output_name handle IO.Io _ => "";
    1.42 +    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    1.43 +    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    1.44 +  in (output, rc) end;
    1.45 +
    1.46 +end;
    1.47 +