12 end; |
12 end; |
13 |
13 |
14 structure SystemProcess: SYSTEM_PROCESS = |
14 structure SystemProcess: SYSTEM_PROCESS = |
15 struct |
15 struct |
16 |
16 |
17 fun system_out cmdline = uninterruptible (fn restore_attributes => fn () => |
17 fun system_out script = uninterruptible (fn restore_attributes => fn () => |
18 let |
18 let |
19 val _ = Secure.deny_secure "Cannot execute shell commands in secure mode"; |
19 val _ = Secure.deny_secure "Cannot execute shell commands in secure mode"; |
20 |
20 |
21 val proc = Unix.execute (cmdline, []); |
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]); |
22 val (proc_stdout, proc_stdin) = Unix.streamsOf proc; |
29 val (proc_stdout, proc_stdin) = Unix.streamsOf proc; |
23 |
30 |
24 fun read buf = |
31 fun read buf = |
25 (case Exn.capture (restore_attributes TextIO.input) proc_stdout of |
32 (case Exn.capture (restore_attributes TextIO.input) proc_stdout of |
26 Exn.Exn Interrupt => (Unix.kill (proc, Posix.Signal.int); read buf) |
33 Exn.Exn Interrupt => (Unix.kill (proc, Posix.Signal.int); read buf) |
27 | Exn.Exn _ => buf |
34 | Exn.Exn _ => buf |
28 | Exn.Result "" => buf |
35 | Exn.Result "" => buf |
29 | Exn.Result txt => read (Buffer.add txt buf)); |
36 | Exn.Result txt => read (Buffer.add txt buf)); |
|
37 |
30 val output = read Buffer.empty; |
38 val output = read Buffer.empty; |
31 val status = Unix.reap proc; |
39 val status = Unix.reap proc; |
32 val rc = Unix.fromStatus status; |
40 val rc = Unix.fromStatus status; |
|
41 |
|
42 val _ = OS.FileSys.remove script_file; |
|
43 val _ = OS.FileSys.remove perl_file; |
33 in |
44 in |
34 if rc = Unix.W_SIGNALED Posix.Signal.int orelse rc = Unix.W_EXITSTATUS 0wx82 |
45 if rc = Unix.W_SIGNALED Posix.Signal.int orelse rc = Unix.W_EXITSTATUS 0wx82 |
35 then raise Interrupt |
46 then raise Interrupt |
36 else (Buffer.content output, if OS.Process.isSuccess status then 0 else 1) |
47 else (Buffer.content output, if OS.Process.isSuccess status then 0 else 1) |
37 end) (); |
48 end) (); |
38 |
49 |
39 fun system cmdline = |
50 fun system script = |
40 let val (output, status) = system_out cmdline in writeln output; status end; |
51 let val (output, status) = system_out script in writeln output; status end; |
41 |
52 |
42 end; |
53 end; |
43 |
54 |