author | wenzelm |
Mon, 08 Aug 2011 13:40:24 +0200 | |
changeset 44054 | da5fcc0f6c52 |
parent 43850 | 7f2cbc713344 |
child 47499 | 4b0daca2bf88 |
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 |
||
44054 | 8 |
signature BASH = |
9 |
sig |
|
10 |
val process: string -> {output: string, rc: int, terminate: unit -> unit} |
|
11 |
end; |
|
12 |
||
13 |
structure Bash: BASH = |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
14 |
struct |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
15 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
16 |
fun process script = |
26220 | 17 |
let |
40749 | 18 |
val id = serial_string (); |
19 |
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
20 |
val output_path = File.tmp_path (Path.basic ("bash_output" ^ id)); |
|
21 |
fun cleanup () = (try File.rm script_path; try File.rm output_path); |
|
22 |
in |
|
23 |
let |
|
24 |
val _ = File.write script_path script; |
|
25 |
val status = |
|
26 |
OS.Process.system |
|
27 |
("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ |
|
28 |
" script \"exec bash " ^ File.shell_path script_path ^ " > " ^ |
|
29 |
File.shell_path output_path ^ "\""); |
|
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)); |
|
26220 | 36 |
|
40749 | 37 |
val output = the_default "" (try File.read output_path); |
38 |
val _ = cleanup (); |
|
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40749
diff
changeset
|
39 |
in {output = output, rc = rc, terminate = fn () => ()} end |
40749 | 40 |
handle exn => (cleanup (); reraise exn) |
41 |
end; |
|
26220 | 42 |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
43 |
end; |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
44 |