more operations (as in ML);

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