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