src/Pure/General/exn.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/exn.scala	Sat Dec 19 16:02:26 2009 +0100
@@ -0,0 +1,28 @@
+/*  Title:      Pure/General/exn.scala
+    Author:     Makarius
+
+Extra support for exceptions.
+*/
+
+package isabelle
+
+
+object Exn
+{
+  /* runtime exceptions as values */
+
+  sealed abstract class Result[A]
+  case class Res[A](val result: A) extends Result[A]
+  case class Exn[A](val exn: Exception) extends Result[A]
+
+  def capture[A](e: => A): Result[A] =
+    try { Res(e) }
+    catch { case exn: RuntimeException => Exn[A](exn) }
+
+  def release[A](result: Result[A]): A =
+    result match {
+      case Res(x) => x
+      case Exn(exn) => throw exn
+    }
+}
+