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