src/Pure/ML-Systems/system_shell.ML
author wenzelm
Thu Mar 06 20:17:50 2008 +0100 (2008-03-06)
changeset 26220 d34b68c21f9a
child 26504 6e87c0a60104
permissions -rw-r--r--
common setup for system_out/system;
     1 (*  Title:      Pure/ML-Systems/system_shell.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Generic system shell processes (no provisions to propagate interrupts;
     6 might still work via the controlling tty).
     7 *)
     8 
     9 local
    10 
    11 fun read_file name =
    12   let val is = TextIO.openIn name
    13   in TextIO.inputAll is before TextIO.closeIn is end;
    14 
    15 fun write_file name txt =
    16   let val os = TextIO.openOut name
    17   in TextIO.output (os, txt) before TextIO.closeOut os end;
    18 
    19 in
    20 
    21 fun system_out script =
    22   let
    23     val script_name = OS.FileSys.tmpName ();
    24     val _ = write_file script_name script;
    25 
    26     val output_name = OS.FileSys.tmpName ();
    27 
    28     val status =
    29       OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
    30         script_name ^ " /dev/null " ^ output_name);
    31     val rc =
    32       (case Posix.Process.fromStatus status of
    33         Posix.Process.W_EXITED => 0
    34       | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    35       | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    36       | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    37 
    38     val output = read_file output_name handle IO.Io _ => "";
    39     val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    40     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    41   in (output, rc) end;
    42 
    43 end;
    44