9 val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
9 val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
10 end; |
10 end; |
11 |
11 |
12 structure Bash: BASH = |
12 structure Bash: BASH = |
13 struct |
13 struct |
14 |
|
15 fun cygwin_bash arg = |
|
16 let val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe" |
|
17 in Windows.simpleExecute (cmd, quote cmd ^ " -c " ^ quote arg) end; |
|
18 |
14 |
19 val process = uninterruptible (fn restore_attributes => fn script => |
15 val process = uninterruptible (fn restore_attributes => fn script => |
20 let |
16 let |
21 datatype result = Wait | Signal | Result of int; |
17 datatype result = Wait | Signal | Result of int; |
22 val result = Synchronized.var "bash_result" Wait; |
18 val result = Synchronized.var "bash_result" Wait; |
37 val system_thread = |
33 val system_thread = |
38 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
34 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
39 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
35 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
40 let |
36 let |
41 val _ = File.write script_path script; |
37 val _ = File.write script_path script; |
|
38 val bash_script = |
|
39 "bash " ^ File.shell_path script_path ^ |
|
40 " > " ^ File.shell_path out_path ^ |
|
41 " 2> " ^ File.shell_path err_path; |
|
42 val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; |
42 val rc = |
43 val rc = |
43 cygwin_bash |
44 Windows.simpleExecute ("", |
44 ("echo $$ > " ^ File.shell_path pid_path ^ "; exec bash " ^ |
45 quote (ML_System.platform_path bash_process) ^ " " ^ |
45 File.shell_path script_path ^ |
46 quote (File.platform_path pid_path) ^ " bash -c " ^ quote bash_script) |
46 " > " ^ File.shell_path out_path ^ |
|
47 " 2> " ^ File.shell_path err_path) |
|
48 |> Windows.fromStatus |> SysWord.toInt; |
47 |> Windows.fromStatus |> SysWord.toInt; |
49 val res = if rc = 130 orelse rc = 512 then Signal else Result rc; |
48 val res = if rc = 130 orelse rc = 512 then Signal else Result rc; |
50 in Synchronized.change result (K res) end |
49 in Synchronized.change result (K res) end |
51 handle exn => |
50 handle exn => |
52 (Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); |
51 (Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); |
59 |
58 |
60 fun terminate NONE = () |
59 fun terminate NONE = () |
61 | terminate (SOME pid) = |
60 | terminate (SOME pid) = |
62 let |
61 let |
63 fun kill s = |
62 fun kill s = |
64 OS.Process.isSuccess (cygwin_bash ("kill -" ^ s ^ " -" ^ string_of_int pid)) |
63 let |
65 handle OS.SysErr _ => false; |
64 val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; |
|
65 val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; |
|
66 in |
|
67 OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) |
|
68 handle OS.SysErr _ => false |
|
69 end; |
|
70 |
66 fun multi_kill count s = |
71 fun multi_kill count s = |
67 count = 0 orelse |
72 count = 0 orelse |
68 (kill s; kill "0") andalso |
73 (kill s; kill "0") andalso |
69 (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
74 (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
70 val _ = |
75 val _ = |