src/Pure/General/exn.scala
author wenzelm
Sun, 02 Oct 2016 21:05:14 +0200
changeset 63999 5649a993666d
parent 63782 aced4f0d1ad4
child 64370 865b39487b5d
permissions -rw-r--r--
more operations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62508
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents: 62492
diff changeset
     1
/*  Title:      Pure/General/exn.scala
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
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
{
62492
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    13
  /* user errors */
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    14
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    15
  class User_Error(message: String) extends RuntimeException(message)
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    16
  {
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    17
    override def equals(that: Any): Boolean =
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    18
      that match {
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    19
        case other: User_Error => message == other.getMessage
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    20
        case _ => false
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    21
      }
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    22
    override def hashCode: Int = message.hashCode
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    23
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    24
    override def toString: String = "ERROR(" + message + ")"
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    25
  }
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    26
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    27
  object ERROR
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    28
  {
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    29
    def apply(message: String): User_Error = new User_Error(message)
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    30
    def unapply(exn: Throwable): Option[String] = user_message(exn)
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    31
  }
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    32
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    33
  def error(message: String): Nothing = throw ERROR(message)
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    34
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    35
  def cat_message(msg1: String, msg2: String): String =
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    36
    if (msg1 == "") msg2
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    37
    else if (msg2 == "") msg1
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    38
    else msg1 + "\n" + msg2
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    39
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    40
  def cat_error(msg1: String, msg2: String): Nothing =
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    41
    error(cat_message(msg1, msg2))
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    42
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
    43
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    44
  /* exceptions as values */
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    45
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    46
  sealed abstract class Result[A]
59698
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    47
  {
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    48
    def user_error: Result[A] =
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    49
      this match {
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    50
        case Exn(ERROR(msg)) => Exn(ERROR(msg))
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    51
        case _ => this
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    52
      }
d4ce901f20c5 value-oriented user error, for well-defined Thy_Syntax.chop_common;
wenzelm
parents: 59697
diff changeset
    53
  }
43762
wenzelm
parents: 43761
diff changeset
    54
  case class Res[A](res: A) extends Result[A]
wenzelm
parents: 43761
diff changeset
    55
  case class Exn[A](exn: Throwable) extends Result[A]
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    56
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    57
  def capture[A](e: => A): Result[A] =
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    58
    try { Res(e) }
34313
2f890016afab treat *all* JVM throwables as "exceptions", cf. ML version;
wenzelm
parents: 34300
diff changeset
    59
    catch { case exn: Throwable => Exn[A](exn) }
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    60
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    61
  def release[A](result: Result[A]): A =
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    62
    result match {
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    63
      case Res(x) => x
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    64
      case Exn(exn) => throw exn
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    65
    }
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    66
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents: 57831
diff changeset
    67
  def release_first[A](results: List[Result[A]]): List[A] =
59138
wenzelm
parents: 59136
diff changeset
    68
    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
wenzelm
parents: 59136
diff changeset
    69
      case Some(Exn(exn)) => throw exn
wenzelm
parents: 59136
diff changeset
    70
      case _ => results.map(release(_))
wenzelm
parents: 59136
diff changeset
    71
    }
59136
c2b23cb8a677 added Par_List in Scala, in accordance to ML version;
wenzelm
parents: 57831
diff changeset
    72
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
    73
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    74
  /* interrupts */
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    75
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    76
  def is_interrupt(exn: Throwable): Boolean =
56670
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    77
  {
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    78
    var found_interrupt = false
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    79
    var e = exn
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    80
    while (!found_interrupt && e != null) {
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    81
      found_interrupt |= e.isInstanceOf[InterruptedException]
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    82
      e = e.getCause
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    83
    }
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    84
    found_interrupt
3f23441453d0 detect nested interrupts;
wenzelm
parents: 56667
diff changeset
    85
  }
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    86
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    87
  object Interrupt
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    88
  {
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    89
    def apply(): Throwable = new InterruptedException
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    90
    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
    91
61558
wenzelm
parents: 59698
diff changeset
    92
    def expose() { if (Thread.interrupted) throw apply() }
56861
5f827142d89a tuned signature;
wenzelm
parents: 56860
diff changeset
    93
    def impose() { Thread.currentThread.interrupt }
56860
dc71c3d0e909 tuned signature;
wenzelm
parents: 56782
diff changeset
    94
56862
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
    95
    def postpone[A](body: => A): Option[A] =
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
    96
    {
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
    97
      val interrupted = Thread.interrupted
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
    98
      val result = capture { body }
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
    99
      if (interrupted) impose()
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   100
      result match {
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   101
        case Res(x) => Some(x)
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   102
        case Exn(e) =>
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   103
          if (is_interrupt(e)) { impose(); None }
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   104
          else throw e
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   105
      }
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   106
    }
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56861
diff changeset
   107
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   108
    val return_code = 130
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   109
  }
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   110
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   111
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   112
  /* POSIX return code */
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   113
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   114
  def return_code(exn: Throwable, rc: Int): Int =
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   115
    if (is_interrupt(exn)) Interrupt.return_code else rc
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   116
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   117
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
   118
  /* message */
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
   119
48479
819f7a5f3e7f more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents: 48476
diff changeset
   120
  def user_message(exn: Throwable): Option[String] =
59697
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   121
    if (exn.getClass == classOf[RuntimeException] ||
62492
0e53fade87fe clarified modules;
wenzelm
parents: 61925
diff changeset
   122
        exn.getClass == classOf[User_Error])
59697
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   123
    {
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
   124
      val msg = exn.getMessage
57831
885888a880fb more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
wenzelm
parents: 56862
diff changeset
   125
      Some(if (msg == null || msg == "") "Error" else msg)
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43762
diff changeset
   126
    }
63782
aced4f0d1ad4 clarified exceptions;
wenzelm
parents: 62508
diff changeset
   127
    else if (exn.isInstanceOf[java.sql.SQLException])
aced4f0d1ad4 clarified exceptions;
wenzelm
parents: 62508
diff changeset
   128
    {
aced4f0d1ad4 clarified exceptions;
wenzelm
parents: 62508
diff changeset
   129
      val msg = exn.getMessage
aced4f0d1ad4 clarified exceptions;
wenzelm
parents: 62508
diff changeset
   130
      Some(if (msg == null || msg == "") "SQL error" else msg)
aced4f0d1ad4 clarified exceptions;
wenzelm
parents: 62508
diff changeset
   131
    }
59697
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   132
    else if (exn.isInstanceOf[java.io.IOException])
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   133
    {
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   134
      val msg = exn.getMessage
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   135
      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
43e14b0e2ef8 more explicit exception User_Error, with value-oriented equality;
wenzelm
parents: 59138
diff changeset
   136
    }
48479
819f7a5f3e7f more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents: 48476
diff changeset
   137
    else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
819f7a5f3e7f more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents: 48476
diff changeset
   138
    else None
819f7a5f3e7f more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents: 48476
diff changeset
   139
819f7a5f3e7f more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents: 48476
diff changeset
   140
  def message(exn: Throwable): String =
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 52066
diff changeset
   141
    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   142
}