| author | blanchet | 
| Thu, 29 Jul 2010 22:13:15 +0200 | |
| changeset 38099 | e3bb96b83807 | 
| parent 34313 | 2f890016afab | 
| child 43761 | e72ba84ae58f | 
| permissions | -rw-r--r-- | 
| 34136 | 1 | /* Title: Pure/General/exn.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 34313 
2f890016afab
treat *all* JVM throwables as "exceptions", cf. ML version;
 wenzelm parents: 
34300diff
changeset | 4 | Extra support for exceptions (arbitrary throwables). | 
| 34136 | 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] | |
| 34313 
2f890016afab
treat *all* JVM throwables as "exceptions", cf. ML version;
 wenzelm parents: 
34300diff
changeset | 16 | case class Exn[A](val exn: Throwable) extends Result[A] | 
| 34136 | 17 | |
| 18 | def capture[A](e: => A): Result[A] = | |
| 19 |     try { Res(e) }
 | |
| 34313 
2f890016afab
treat *all* JVM throwables as "exceptions", cf. ML version;
 wenzelm parents: 
34300diff
changeset | 20 |     catch { case exn: Throwable => Exn[A](exn) }
 | 
| 34136 | 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 |