src/Pure/General/exn.scala

support for completion within the formal context;
tuned signature;

/*  Title:      Pure/General/exn.scala
    Module:     PIDE
    Author:     Makarius

Support for exceptions (arbitrary throwables).
*/

package isabelle


object Exn
{
  /* exceptions as values */

  sealed abstract class Result[A]
  case class Res[A](res: A) extends Result[A]
  case class Exn[A](exn: Throwable) extends Result[A]

  def capture[A](e: => A): Result[A] =
    try { Res(e) }
    catch { case exn: Throwable => Exn[A](exn) }

  def release[A](result: Result[A]): A =
    result match {
      case Res(x) => x
      case Exn(exn) => throw exn
    }


  /* message */

  private val runtime_exception = Class.forName("java.lang.RuntimeException")

  def user_message(exn: Throwable): Option[String] =
    if (exn.isInstanceOf[java.io.IOException]) {
      val msg = exn.getMessage
      Some(if (msg == null) "I/O error" else "I/O error: " + msg)
    }
    else if (exn.getClass == runtime_exception) {
      val msg = exn.getMessage
      Some(if (msg == null) "Error" else msg)
    }
    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
    else None

  def message(exn: Throwable): String =
    user_message(exn) getOrElse
      (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
       else exn.toString)
}