equal
deleted
inserted
replaced
1 /* Title: Pure/General/exn.scala |
1 /* Title: Pure/General/exn.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Extra support for exceptions. |
4 Extra support for exceptions (arbitrary throwables). |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
11 { |
11 { |
12 /* runtime exceptions as values */ |
12 /* runtime exceptions as values */ |
13 |
13 |
14 sealed abstract class Result[A] |
14 sealed abstract class Result[A] |
15 case class Res[A](val result: A) extends Result[A] |
15 case class Res[A](val result: A) extends Result[A] |
16 case class Exn[A](val exn: Exception) extends Result[A] |
16 case class Exn[A](val exn: Throwable) extends Result[A] |
17 |
17 |
18 def capture[A](e: => A): Result[A] = |
18 def capture[A](e: => A): Result[A] = |
19 try { Res(e) } |
19 try { Res(e) } |
20 catch { case exn: RuntimeException => Exn[A](exn) } // FIXME *all* exceptions (!?), cf. ML version |
20 catch { case exn: Throwable => Exn[A](exn) } |
21 |
21 |
22 def release[A](result: Result[A]): A = |
22 def release[A](result: Result[A]): A = |
23 result match { |
23 result match { |
24 case Res(x) => x |
24 case Res(x) => x |
25 case Exn(exn) => throw exn |
25 case Exn(exn) => throw exn |