1 (* Title: Pure/Concurrent/bash_sequential.ML |
|
2 Author: Makarius |
|
3 |
|
4 Generic GNU bash processes (no provisions to propagate interrupts, but |
|
5 could work via the controlling tty). |
|
6 *) |
|
7 |
|
8 signature BASH = |
|
9 sig |
|
10 val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
|
11 end; |
|
12 |
|
13 structure Bash: BASH = |
|
14 struct |
|
15 |
|
16 fun process script = |
|
17 let |
|
18 val id = serial_string (); |
|
19 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
20 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
|
21 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
|
22 fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path); |
|
23 in |
|
24 let |
|
25 val _ = File.write script_path script; |
|
26 val status = |
|
27 OS.Process.system |
|
28 ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ |
|
29 " script \"exec bash " ^ File.shell_path script_path ^ |
|
30 " > " ^ File.shell_path out_path ^ |
|
31 " 2> " ^ File.shell_path err_path ^ "\""); |
|
32 val rc = |
|
33 (case Posix.Process.fromStatus status of |
|
34 Posix.Process.W_EXITED => 0 |
|
35 | Posix.Process.W_EXITSTATUS w => Word8.toInt w |
|
36 | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) |
|
37 | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s)); |
|
38 |
|
39 val out = the_default "" (try File.read out_path); |
|
40 val err = the_default "" (try File.read err_path); |
|
41 val _ = cleanup (); |
|
42 in {out = out, err = err, rc = rc, terminate = fn () => ()} end |
|
43 handle exn => (cleanup (); reraise exn) |
|
44 end; |
|
45 |
|
46 end; |
|
47 |
|