1 (* Title: Pure/General/system_process.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 System shell processes, with static input/output and propagation of interrupts. |
|
6 *) |
|
7 |
|
8 signature SYSTEM_PROCESS = |
|
9 sig |
|
10 val system_out: string -> string * int |
|
11 val system: string -> int |
|
12 end; |
|
13 |
|
14 structure SystemProcess: SYSTEM_PROCESS = |
|
15 struct |
|
16 |
|
17 fun system_out script = uninterruptible (fn restore_attributes => fn () => |
|
18 let |
|
19 val _ = Secure.deny_secure "Cannot execute shell commands in secure mode"; |
|
20 |
|
21 val script_file = OS.FileSys.tmpName (); |
|
22 val _ = File.write (Path.explode script_file) script; |
|
23 |
|
24 val perl_file = OS.FileSys.tmpName (); |
|
25 val _ = File.write (Path.explode perl_file) (*robust signal handling via perl*) |
|
26 ("$SIG{'INT'} = 'DEFAULT'; exec '/bin/bash --norc " ^ script_file ^ "' || die $!;"); |
|
27 |
|
28 val proc = Unix.execute ("/usr/bin/env", ["perl", "-w", perl_file]); |
|
29 val (proc_stdout, proc_stdin) = Unix.streamsOf proc; |
|
30 |
|
31 fun read buf = |
|
32 (case Exn.capture (restore_attributes TextIO.input) proc_stdout of |
|
33 Exn.Exn Interrupt => (Unix.kill (proc, Posix.Signal.int); read buf) |
|
34 | Exn.Exn _ => buf |
|
35 | Exn.Result "" => buf |
|
36 | Exn.Result txt => read (Buffer.add txt buf)); |
|
37 |
|
38 val output = read Buffer.empty; |
|
39 val status = Unix.reap proc; |
|
40 val rc = Unix.fromStatus status; |
|
41 |
|
42 val _ = OS.FileSys.remove script_file; |
|
43 val _ = OS.FileSys.remove perl_file; |
|
44 in |
|
45 if rc = Unix.W_SIGNALED Posix.Signal.int orelse rc = Unix.W_EXITSTATUS 0wx82 |
|
46 then raise Interrupt |
|
47 else (Buffer.content output, if OS.Process.isSuccess status then 0 else 1) |
|
48 end) (); |
|
49 |
|
50 fun system script = |
|
51 let val (output, status) = system_out script in writeln output; status end; |
|
52 |
|
53 end; |
|
54 |
|