src/Pure/General/exn.scala
author wenzelm
Mon, 28 Nov 2011 22:18:19 +0100
changeset 45667 546d78f0d81f
parent 44158 fe6d1ae7a065
child 45673 cd41e3903fbf
permissions -rw-r--r--
explicit indication of modules for independent Scala library;
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
45667
546d78f0d81f explicit indication of modules for independent Scala library;
wenzelm
parents: 44158
diff changeset
     2
    Module:     Library
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     4
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 34313
diff changeset
     5
Support for exceptions (arbitrary throwables).
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     6
*/
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     7
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     8
package isabelle
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     9
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    10
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    11
object Exn
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    12
{
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    13
  /* exceptions as values */
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    14
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    15
  sealed abstract class Result[A]
43762
wenzelm
parents: 43761
diff changeset
    16
  case class Res[A](res: A) extends Result[A]
wenzelm
parents: 43761
diff changeset
    17
  case class Exn[A](exn: Throwable) extends Result[A]
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    18
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    19
  def capture[A](e: => A): Result[A] =
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    20
    try { Res(e) }
34313
2f890016afab treat *all* JVM throwables as "exceptions", cf. ML version;
wenzelm
parents: 34300
diff changeset
    21
    catch { case exn: Throwable => Exn[A](exn) }
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    22
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    23
  def release[A](result: Result[A]): A =
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    24
    result match {
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    25
      case Res(x) => x
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    26
      case Exn(exn) => throw exn
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    27
    }
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    28
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    29
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    30
  /* message */
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    31
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    32
  private val runtime_exception = Class.forName("java.lang.RuntimeException")
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    33
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    34
  def message(exn: Throwable): String =
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    35
    if (exn.getClass == runtime_exception) {
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    36
      val msg = exn.getMessage
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    37
      if (msg == null) "Error" else msg
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    38
    }
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    39
    else exn.toString
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    40
}
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    41