--- 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
}