src/Pure/ML-Systems/system_shell.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 29564 f8b933a62151
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      Pure/ML-Systems/system_shell.ML
     2     Author:     Makarius
     3 
     4 Generic system shell processes (no provisions to propagate interrupts;
     5 might still work via the controlling tty).
     6 *)
     7 
     8 local
     9 
    10 fun read_file name =
    11   let val is = TextIO.openIn name
    12   in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
    13 
    14 fun write_file name txt =
    15   let val os = TextIO.openOut name
    16   in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    17 
    18 in
    19 
    20 fun system_out script =
    21   let
    22     val script_name = OS.FileSys.tmpName ();
    23     val _ = write_file script_name script;
    24 
    25     val output_name = OS.FileSys.tmpName ();
    26 
    27     val status =
    28       OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
    29         script_name ^ " /dev/null " ^ output_name);
    30     val rc =
    31       (case Posix.Process.fromStatus status of
    32         Posix.Process.W_EXITED => 0
    33       | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    34       | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    35       | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    36 
    37     val output = read_file output_name handle IO.Io _ => "";
    38     val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    39     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    40   in (output, rc) end;
    41 
    42 end;
    43