src/Pure/General/exn.scala
author wenzelm
Sat, 19 Dec 2009 16:02:26 +0100
changeset 34136 3dcb46ae6185
child 34300 3f2e25dc99ab
permissions -rw-r--r--
added basic library -- Scala version; added extra support for exceptions -- Scala version; moved exn.ML to accompany exn.scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/exn.scala
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     3
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     4
Extra support for exceptions.
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     5
*/
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     6
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     7
package isabelle
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     8
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     9
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    10
object Exn
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    11
{
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    12
  /* runtime exceptions as values */
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    13
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    14
  sealed abstract class Result[A]
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    15
  case class Res[A](val result: A) extends Result[A]
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    16
  case class Exn[A](val exn: Exception) extends Result[A]
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    17
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    18
  def capture[A](e: => A): Result[A] =
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    19
    try { Res(e) }
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    20
    catch { case exn: RuntimeException => Exn[A](exn) }
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    21
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    22
  def release[A](result: Result[A]): A =
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    23
    result match {
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    24
      case Res(x) => x
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    25
      case Exn(exn) => throw exn
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    26
    }
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    27
}
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    28