author | huffman |
Mon, 20 Dec 2010 07:50:47 -0800 | |
changeset 41320 | 4953e21ac76c |
parent 40749 | cb6698d2dbaf |
child 43847 | 529159f81d06 |
permissions | -rw-r--r-- |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
39583
diff
changeset
|
1 |
(* Title: Pure/Concurrent/bash_sequential.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 |
||
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
|
8 |
fun bash_output script = |
26220 | 9 |
let |
40749 | 10 |
val id = serial_string (); |
11 |
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
12 |
val output_path = File.tmp_path (Path.basic ("bash_output" ^ id)); |
|
13 |
fun cleanup () = (try File.rm script_path; try File.rm output_path); |
|
14 |
in |
|
15 |
let |
|
16 |
val _ = File.write script_path script; |
|
17 |
val status = |
|
18 |
OS.Process.system |
|
19 |
("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ |
|
20 |
" script \"exec bash " ^ File.shell_path script_path ^ " > " ^ |
|
21 |
File.shell_path output_path ^ "\""); |
|
22 |
val rc = |
|
23 |
(case Posix.Process.fromStatus status of |
|
24 |
Posix.Process.W_EXITED => 0 |
|
25 |
| Posix.Process.W_EXITSTATUS w => Word8.toInt w |
|
26 |
| Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) |
|
27 |
| Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s)); |
|
26220 | 28 |
|
40749 | 29 |
val output = the_default "" (try File.read output_path); |
30 |
val _ = cleanup (); |
|
31 |
in (output, rc) end |
|
32 |
handle exn => (cleanup (); reraise exn) |
|
33 |
end; |
|
26220 | 34 |