clarified process interrupt: exactly one signal (like thread interrupt);
authorwenzelm
Tue, 08 Mar 2016 17:55:11 +0100
changeset 62558 c46418f12ee1
parent 62557 a4ea3a222e0e
child 62559 83e815849a91
clarified process interrupt: exactly one signal (like thread interrupt);
src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Tue Mar 08 17:52:33 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Tue Mar 08 17:55:11 2016 +0100
@@ -59,6 +59,9 @@
 
     private val pid = stdout.readLine
 
+    def interrupt()
+    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
+
     private def kill(signal: String): Boolean =
       Exn.Interrupt.postpone {
         Isabelle_System.kill(signal, pid)
@@ -80,7 +83,6 @@
       running
     }
 
-    def interrupt() { multi_kill("INT") }
     def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }