src/Pure/General/exn.scala
changeset 71705 7b75d52a1bf1
parent 71700 6c39c3be85df
child 72335 b8708212bdd5
--- 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
   }