src/Pure/General/exn.scala
author wenzelm
Tue Nov 03 16:35:00 2015 +0100 (2015-11-03)
changeset 61558 68b86028e02a
parent 59698 d4ce901f20c5
permissions -rw-r--r--
tuned;
wenzelm@34136
     1
/*  Title:      Pure/General/exn.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@34136
     3
    Author:     Makarius
wenzelm@34136
     4
wenzelm@43761
     5
Support for exceptions (arbitrary throwables).
wenzelm@34136
     6
*/
wenzelm@34136
     7
wenzelm@34136
     8
package isabelle
wenzelm@34136
     9
wenzelm@34136
    10
wenzelm@34136
    11
object Exn
wenzelm@34136
    12
{
wenzelm@44158
    13
  /* exceptions as values */
wenzelm@34136
    14
wenzelm@34136
    15
  sealed abstract class Result[A]
wenzelm@59698
    16
  {
wenzelm@59698
    17
    def user_error: Result[A] =
wenzelm@59698
    18
      this match {
wenzelm@59698
    19
        case Exn(ERROR(msg)) => Exn(ERROR(msg))
wenzelm@59698
    20
        case _ => this
wenzelm@59698
    21
      }
wenzelm@59698
    22
  }
wenzelm@43762
    23
  case class Res[A](res: A) extends Result[A]
wenzelm@43762
    24
  case class Exn[A](exn: Throwable) extends Result[A]
wenzelm@34136
    25
wenzelm@34136
    26
  def capture[A](e: => A): Result[A] =
wenzelm@34136
    27
    try { Res(e) }
wenzelm@34313
    28
    catch { case exn: Throwable => Exn[A](exn) }
wenzelm@34136
    29
wenzelm@34136
    30
  def release[A](result: Result[A]): A =
wenzelm@34136
    31
    result match {
wenzelm@34136
    32
      case Res(x) => x
wenzelm@34136
    33
      case Exn(exn) => throw exn
wenzelm@34136
    34
    }
wenzelm@44158
    35
wenzelm@59136
    36
  def release_first[A](results: List[Result[A]]): List[A] =
wenzelm@59138
    37
    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
wenzelm@59138
    38
      case Some(Exn(exn)) => throw exn
wenzelm@59138
    39
      case _ => results.map(release(_))
wenzelm@59138
    40
    }
wenzelm@59136
    41
wenzelm@44158
    42
wenzelm@56667
    43
  /* interrupts */
wenzelm@56667
    44
wenzelm@56667
    45
  def is_interrupt(exn: Throwable): Boolean =
wenzelm@56670
    46
  {
wenzelm@56670
    47
    var found_interrupt = false
wenzelm@56670
    48
    var e = exn
wenzelm@56670
    49
    while (!found_interrupt && e != null) {
wenzelm@56670
    50
      found_interrupt |= e.isInstanceOf[InterruptedException]
wenzelm@56670
    51
      e = e.getCause
wenzelm@56670
    52
    }
wenzelm@56670
    53
    found_interrupt
wenzelm@56670
    54
  }
wenzelm@56667
    55
wenzelm@56667
    56
  object Interrupt
wenzelm@56667
    57
  {
wenzelm@56667
    58
    def apply(): Throwable = new InterruptedException
wenzelm@56667
    59
    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
wenzelm@56667
    60
wenzelm@61558
    61
    def expose() { if (Thread.interrupted) throw apply() }
wenzelm@56861
    62
    def impose() { Thread.currentThread.interrupt }
wenzelm@56860
    63
wenzelm@56862
    64
    def postpone[A](body: => A): Option[A] =
wenzelm@56862
    65
    {
wenzelm@56862
    66
      val interrupted = Thread.interrupted
wenzelm@56862
    67
      val result = capture { body }
wenzelm@56862
    68
      if (interrupted) impose()
wenzelm@56862
    69
      result match {
wenzelm@56862
    70
        case Res(x) => Some(x)
wenzelm@56862
    71
        case Exn(e) =>
wenzelm@56862
    72
          if (is_interrupt(e)) { impose(); None }
wenzelm@56862
    73
          else throw e
wenzelm@56862
    74
      }
wenzelm@56862
    75
    }
wenzelm@56862
    76
wenzelm@56667
    77
    val return_code = 130
wenzelm@56667
    78
  }
wenzelm@56667
    79
wenzelm@56667
    80
wenzelm@56667
    81
  /* POSIX return code */
wenzelm@56667
    82
wenzelm@56667
    83
  def return_code(exn: Throwable, rc: Int): Int =
wenzelm@56667
    84
    if (is_interrupt(exn)) Interrupt.return_code else rc
wenzelm@56667
    85
wenzelm@56667
    86
wenzelm@44158
    87
  /* message */
wenzelm@44158
    88
wenzelm@48479
    89
  def user_message(exn: Throwable): Option[String] =
wenzelm@59697
    90
    if (exn.getClass == classOf[RuntimeException] ||
wenzelm@59697
    91
        exn.getClass == classOf[Library.User_Error])
wenzelm@59697
    92
    {
wenzelm@44158
    93
      val msg = exn.getMessage
wenzelm@57831
    94
      Some(if (msg == null || msg == "") "Error" else msg)
wenzelm@44158
    95
    }
wenzelm@59697
    96
    else if (exn.isInstanceOf[java.io.IOException])
wenzelm@59697
    97
    {
wenzelm@59697
    98
      val msg = exn.getMessage
wenzelm@59697
    99
      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
wenzelm@59697
   100
    }
wenzelm@48479
   101
    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
wenzelm@48479
   102
    else None
wenzelm@48479
   103
wenzelm@48479
   104
  def message(exn: Throwable): String =
wenzelm@56667
   105
    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
wenzelm@34136
   106
}