author | wenzelm |
Wed, 22 Sep 2010 00:45:42 +0200 | |
changeset 39583 | c1e9c6dfeff8 |
parent 39576 | 48baf61cb888 |
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 = |
|
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39576
diff
changeset
|
28 |
OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39576
diff
changeset
|
29 |
" script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); |
26220 | 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 |