src/Pure/General/exn.scala
author wenzelm
Sun, 27 Dec 2009 21:33:35 +0100
changeset 34187 7b659c1561f1
parent 34136 3dcb46ae6185
child 34300 3f2e25dc99ab
permissions -rw-r--r--
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

/*  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
    }
}