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 }