34136
|
1 |
/* Title: Pure/General/exn.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Extra support for exceptions.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
object Exn
|
|
11 |
{
|
|
12 |
/* runtime exceptions as values */
|
|
13 |
|
|
14 |
sealed abstract class Result[A]
|
|
15 |
case class Res[A](val result: A) extends Result[A]
|
|
16 |
case class Exn[A](val exn: Exception) extends Result[A]
|
|
17 |
|
|
18 |
def capture[A](e: => A): Result[A] =
|
|
19 |
try { Res(e) }
|
|
20 |
catch { case exn: RuntimeException => Exn[A](exn) }
|
|
21 |
|
|
22 |
def release[A](result: Result[A]): A =
|
|
23 |
result match {
|
|
24 |
case Res(x) => x
|
|
25 |
case Exn(exn) => throw exn
|
|
26 |
}
|
|
27 |
}
|
|
28 |
|