--- a/src/Pure/System/bash.ML Sun Feb 07 12:55:41 2021 +0100
+++ b/src/Pure/System/bash.ML Sun Feb 07 15:32:57 2021 +0100
@@ -11,11 +11,33 @@
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
+structure Bash: sig val terminate: int option -> unit end =
+struct
+
+fun terminate NONE = ()
+ | terminate (SOME pid) =
+ let
+ val kill = Kill.kill_group pid;
+
+ fun multi_kill count s =
+ count = 0 orelse
+ (kill s; kill Kill.SIGNONE) andalso
+ (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+ val _ =
+ multi_kill 10 Kill.SIGINT andalso
+ multi_kill 10 Kill.SIGTERM andalso
+ multi_kill 10 Kill.SIGKILL;
+ in () end;
+
+end;
+
if ML_System.platform_is_windows then ML
\<open>
structure Bash: BASH =
struct
+open Bash;
+
val string = Bash_Syntax.string;
val strings = Bash_Syntax.strings;
@@ -63,28 +85,6 @@
NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
| some => some);
- fun terminate NONE = ()
- | terminate (SOME pid) =
- let
- fun kill s =
- let
- val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
- val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
- in
- OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
- handle OS.SysErr _ => false
- end;
-
- fun multi_kill count s =
- count = 0 orelse
- (kill s; kill "0") andalso
- (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
- val _ =
- multi_kill 10 "INT" andalso
- multi_kill 10 "TERM" andalso
- multi_kill 10 "KILL";
- in () end;
-
fun cleanup () =
(Isabelle_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());
@@ -110,6 +110,8 @@
structure Bash: BASH =
struct
+open Bash;
+
val string = Bash_Syntax.string;
val strings = Bash_Syntax.strings;
@@ -163,24 +165,6 @@
NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
| some => some);
- fun terminate NONE = ()
- | terminate (SOME pid) =
- let
- fun kill s =
- (Posix.Process.kill
- (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
- handle OS.SysErr _ => false;
-
- fun multi_kill count s =
- count = 0 orelse
- (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
- (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
- val _ =
- multi_kill 10 Posix.Signal.int andalso
- multi_kill 10 Posix.Signal.term andalso
- multi_kill 10 Posix.Signal.kill;
- in () end;
-
fun cleanup () =
(Isabelle_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());