src/Pure/ML-Systems/system_shell.ML
changeset 26220 d34b68c21f9a
child 26504 6e87c0a60104
equal deleted inserted replaced
26219:2d026932f710 26220:d34b68c21f9a
       
     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