author | wenzelm |
Sat, 06 Feb 2010 14:50:55 +0100 | |
changeset 35010 | d6e492cea6e4 |
parent 29564 | src/Pure/ML-Systems/system_shell.ML@f8b933a62151 |
child 35023 | 16f9877abf0b |
permissions | -rw-r--r-- |
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
29564
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/bash.ML |
26220 | 2 |
Author: Makarius |
3 |
||
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
29564
diff
changeset
|
4 |
Generic GNU bash processes (no provisions to propagate interrupts, but |
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
29564
diff
changeset
|
5 |
could work via the controlling tty). |
26220 | 6 |
*) |
7 |
||
8 |
local |
|
9 |
||
10 |
fun read_file name = |
|
11 |
let val is = TextIO.openIn name |
|
26504 | 12 |
in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; |
26220 | 13 |
|
14 |
fun write_file name txt = |
|
15 |
let val os = TextIO.openOut name |
|
26504 | 16 |
in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; |
26220 | 17 |
|
18 |
in |
|
19 |
||
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
29564
diff
changeset
|
20 |
fun bash_output script = |
26220 | 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 |