# HG changeset patch
# User wenzelm
# Date 1361638071 -3600
# Node ID ee836df361ed419157d6f5ac28754e6129d0ed0d
# Parent  9db9e8c608ea890cfdffe3dc6f44abe8788e5ffa
more robust handling of repeated interrupts while terminating managed process;
NB: InterruptedException should have interrupted status cleared already;

diff -r 9db9e8c608ea -r ee836df361ed src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Feb 23 17:12:48 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 23 17:47:51 2013 +0100
@@ -298,8 +298,11 @@
 
     private def kill(signal: String): Boolean =
     {
-      execute(true, "kill", "-" + signal, "-" + pid).waitFor
-      execute(true, "kill", "-0", "-" + pid).waitFor == 0
+      try {
+        execute(true, "kill", "-" + signal, "-" + pid).waitFor
+        execute(true, "kill", "-0", "-" + pid).waitFor == 0
+      }
+      catch { case _: InterruptedException => true }
     }
 
     private def multi_kill(signal: String): Boolean =
@@ -308,7 +311,7 @@
       var count = 10
       while (running && count > 0) {
         if (kill(signal)) {
-          Thread.sleep(100)
+          try { Thread.sleep(100) } catch { case _: InterruptedException => }
           count -= 1
         }
         else running = false
@@ -363,7 +366,7 @@
 
       val rc =
         try { proc.join }
-        catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
+        catch { case e: InterruptedException => proc.terminate; 130 }
       Bash_Result(stdout.join, stderr.join, rc)
     }
   }