--- a/src/Pure/ROOT.ML Sun Feb 07 12:55:41 2021 +0100
+++ b/src/Pure/ROOT.ML Sun Feb 07 15:32:57 2021 +0100
@@ -294,6 +294,7 @@
(*Isabelle system*)
ML_file "PIDE/protocol_command.ML";
ML_file "System/scala.ML";
+ML_file "System/kill.ML";
ML_file "System/bash.ML";
ML_file "System/isabelle_system.ML";
--- 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 ());
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/kill.ML Sun Feb 07 15:32:57 2021 +0100
@@ -0,0 +1,59 @@
+(* Title: Pure/System/kill.ML
+ Author: Makarius
+
+Kill external process group.
+*)
+
+signature KILL =
+sig
+ type signal
+ val SIGNONE: signal
+ val SIGINT: signal
+ val SIGTERM: signal
+ val SIGKILL: signal
+ val kill_group: int -> signal -> bool
+end;
+
+if ML_System.platform_is_windows then ML
+\<open>
+structure Kill: KILL =
+struct
+
+type signal = string;
+
+val SIGNONE = "0";
+val SIGINT = "INT";
+val SIGTERM = "TERM";
+val SIGKILL = "KILL";
+
+fun kill_group pid 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;
+
+end;
+\<close>
+else ML
+\<open>
+structure Kill: KILL =
+struct
+
+type signal = Posix.Signal.signal;
+
+val SIGNONE = Posix.Signal.fromWord 0w0;
+val SIGINT = Posix.Signal.int;
+val SIGTERM = Posix.Signal.term;
+val SIGKILL = Posix.Signal.kill;
+
+fun kill_group pid s =
+ let
+ val arg = Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid));
+ val _ = Posix.Process.kill (arg, s);
+ in true end handle OS.SysErr _ => false;
+
+end;
+\<close>