# HG changeset patch # User wenzelm # Date 1586173244 -7200 # Node ID 7b75d52a1bf12e955ebea1cd5e2f1a8d51f4bd49 # Parent b9a5eb0f3b43c51f8dc814f6437fffad6c085183 clarified interrupt handling; diff -r b9a5eb0f3b43 -r 7b75d52a1bf1 src/Pure/General/exn.scala --- 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 } diff -r b9a5eb0f3b43 -r 7b75d52a1bf1 src/Pure/System/bash.scala --- 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