clarified interrupt handling;

--- a/src/Pure/General/exn.scala	Mon Apr 06 12:53:45 2020 +0200
+++ b/src/Pure/General/exn.scala	Mon Apr 06 13:40:44 2020 +0200
@@ -100,19 +100,6 @@
     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
   }
 

--- a/src/Pure/System/bash.scala	Mon Apr 06 12:53:45 2020 +0200
+++ b/src/Pure/System/bash.scala	Mon Apr 06 13:40:44 2020 +0200
@@ -100,13 +100,11 @@
 
     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)
-        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
+    {
+      Isabelle_System.kill(signal, pid)
+      Isabelle_System.kill("0", pid)._2 == 0
+    }
 
     private def multi_kill(signal: String): Boolean =
     {
@@ -114,23 +112,26 @@
       var count = 10
       while (running && count > 0) {
         if (kill(signal)) {
-          Exn.Interrupt.postpone {
-            Time.seconds(0.1).sleep
-            count -= 1
-          }
+          Time.seconds(0.1).sleep
+          count -= 1
         }
         else running = false
       }
       running
     }
 
-    def terminate()
+    def terminate(): Unit = Isabelle_Thread.uninterruptible
     {
       multi_kill("INT") && multi_kill("TERM") && kill("KILL")
       proc.destroy
       do_cleanup()
     }
 
+    def interrupt(): Unit = Isabelle_Thread.uninterruptible
+    {
+      Isabelle_System.kill("INT", pid)
+    }
+
 
     // JVM shutdown hook