src/Pure/General/exn.scala

--- a/src/Pure/General/exn.scala	Mon May 05 09:41:23 2014 +0200
+++ b/src/Pure/General/exn.scala	Mon May 05 10:25:09 2014 +0200
@@ -48,6 +48,19 @@
     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
   }