# HG changeset patch
# User wenzelm
# Date 1527596739 -7200
# Node ID d088799fd278e36fc3b24f175390042b38ee3f51
# Parent  2acbf8129d8bb195589d8a14fe744ea86b5e9b93
more operations (as in ML);

diff -r 2acbf8129d8b -r d088799fd278 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue May 29 13:45:51 2018 +0200
+++ b/src/Pure/General/exn.scala	Tue May 29 14:25:39 2018 +0200
@@ -81,6 +81,10 @@
     found_interrupt
   }
 
+  def interruptible_capture[A](e: => A): Result[A] =
+    try { Res(e) }
+    catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
+
   object Interrupt
   {
     def apply(): Throwable = new InterruptedException