# HG changeset patch
# User wenzelm
# Date 1612708377 -3600
# Node ID 5cb4f7107add394f6a6adb134682512e1be6cebc
# Parent  4c8edf348c4e932ee44c0bb484fa62d6d5d6fee1
clarified modules: less redundancy;

diff -r 4c8edf348c4e -r 5cb4f7107add src/Pure/ROOT.ML
--- 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";
 
diff -r 4c8edf348c4e -r 5cb4f7107add src/Pure/System/bash.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 ());
diff -r 4c8edf348c4e -r 5cb4f7107add src/Pure/System/kill.ML
--- /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>