# HG changeset patch
# User wenzelm
# Date 1399278309 -7200
# Node ID e6f7ed54d64e19c0f2e9be9e0e0cd2ef62ea3754
# Parent  5f827142d89a83e69b5a5e3c54c2c8ff265264f5
more robust process kill -- postpone interrupts on current thread;

diff -r 5f827142d89a -r e6f7ed54d64e src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Mon May 05 09:41:23 2014 +0200
+++ b/src/Pure/General/exn.scala	Mon May 05 10:25:09 2014 +0200
@@ -48,6 +48,19 @@
     def expose() { if (Thread.interrupted()) throw apply() }
     def impose() { Thread.currentThread.interrupt }
 
+    def postpone[A](body: => A): Option[A] =
+    {
+      val interrupted = Thread.interrupted
+      val result = capture { body }
+      if (interrupted) impose()
+      result match {
+        case Res(x) => Some(x)
+        case Exn(e) =>
+          if (is_interrupt(e)) { impose(); None }
+          else throw e
+      }
+    }
+
     val return_code = 130
   }
 
diff -r 5f827142d89a -r e6f7ed54d64e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon May 05 09:41:23 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon May 05 10:25:09 2014 +0200
@@ -327,13 +327,7 @@
       execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
 
     private def kill(signal: String): Boolean =
-    {
-      try {
-        kill_cmd(signal)
-        kill_cmd("0") == 0
-      }
-      catch { case Exn.Interrupt() => true }
-    }
+      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
 
     private def multi_kill(signal: String): Boolean =
     {
@@ -341,8 +335,10 @@
       var count = 10
       while (running && count > 0) {
         if (kill(signal)) {
-          try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
-          count -= 1
+          Exn.Interrupt.postpone {
+            Thread.sleep(100)
+            count -= 1
+          }
         }
         else running = false
       }