src/Pure/ML-Systems/bash.ML
changeset 35010 d6e492cea6e4
parent 29564 f8b933a62151
child 35023 16f9877abf0b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/bash.ML	Sat Feb 06 14:50:55 2010 +0100
     1.3 @@ -0,0 +1,43 @@
     1.4 +(*  Title:      Pure/ML-Systems/bash.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Generic GNU bash processes (no provisions to propagate interrupts, but
     1.8 +could work via the controlling tty).
     1.9 +*)
    1.10 +
    1.11 +local
    1.12 +
    1.13 +fun read_file name =
    1.14 +  let val is = TextIO.openIn name
    1.15 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
    1.16 +
    1.17 +fun write_file name txt =
    1.18 +  let val os = TextIO.openOut name
    1.19 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    1.20 +
    1.21 +in
    1.22 +
    1.23 +fun bash_output script =
    1.24 +  let
    1.25 +    val script_name = OS.FileSys.tmpName ();
    1.26 +    val _ = write_file script_name script;
    1.27 +
    1.28 +    val output_name = OS.FileSys.tmpName ();
    1.29 +
    1.30 +    val status =
    1.31 +      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
    1.32 +        script_name ^ " /dev/null " ^ output_name);
    1.33 +    val rc =
    1.34 +      (case Posix.Process.fromStatus status of
    1.35 +        Posix.Process.W_EXITED => 0
    1.36 +      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    1.37 +      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    1.38 +      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    1.39 +
    1.40 +    val output = read_file output_name handle IO.Io _ => "";
    1.41 +    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    1.42 +    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    1.43 +  in (output, rc) end;
    1.44 +
    1.45 +end;
    1.46 +