author | wenzelm |
Sun, 04 Sep 2016 21:41:08 +0200 | |
changeset 63782 | aced4f0d1ad4 |
parent 62508 | d0b68218ea55 |
child 64370 | 865b39487b5d |
permissions | -rw-r--r-- |
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 | 3 |
Author: Makarius |
4 |
||
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
34313
diff
changeset
|
5 |
Support for exceptions (arbitrary throwables). |
34136 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
object Exn |
|
12 |
{ |
|
62492 | 13 |
/* user errors */ |
14 |
||
15 |
class User_Error(message: String) extends RuntimeException(message) |
|
16 |
{ |
|
17 |
override def equals(that: Any): Boolean = |
|
18 |
that match { |
|
19 |
case other: User_Error => message == other.getMessage |
|
20 |
case _ => false |
|
21 |
} |
|
22 |
override def hashCode: Int = message.hashCode |
|
23 |
||
24 |
override def toString: String = "ERROR(" + message + ")" |
|
25 |
} |
|
26 |
||
27 |
object ERROR |
|
28 |
{ |
|
29 |
def apply(message: String): User_Error = new User_Error(message) |
|
30 |
def unapply(exn: Throwable): Option[String] = user_message(exn) |
|
31 |
} |
|
32 |
||
33 |
def error(message: String): Nothing = throw ERROR(message) |
|
34 |
||
35 |
def cat_message(msg1: String, msg2: String): String = |
|
36 |
if (msg1 == "") msg2 |
|
37 |
else if (msg2 == "") msg1 |
|
38 |
else msg1 + "\n" + msg2 |
|
39 |
||
40 |
def cat_error(msg1: String, msg2: String): Nothing = |
|
41 |
error(cat_message(msg1, msg2)) |
|
42 |
||
43 |
||
44158 | 44 |
/* exceptions as values */ |
34136 | 45 |
|
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 | 54 |
case class Res[A](res: A) extends Result[A] |
55 |
case class Exn[A](exn: Throwable) extends Result[A] |
|
34136 | 56 |
|
57 |
def capture[A](e: => A): Result[A] = |
|
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 | 60 |
|
61 |
def release[A](result: Result[A]): A = |
|
62 |
result match { |
|
63 |
case Res(x) => x |
|
64 |
case Exn(exn) => throw exn |
|
65 |
} |
|
44158 | 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 | 68 |
results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match { |
69 |
case Some(Exn(exn)) => throw exn |
|
70 |
case _ => results.map(release(_)) |
|
71 |
} |
|
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
57831
diff
changeset
|
72 |
|
44158 | 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 | 77 |
{ |
78 |
var found_interrupt = false |
|
79 |
var e = exn |
|
80 |
while (!found_interrupt && e != null) { |
|
81 |
found_interrupt |= e.isInstanceOf[InterruptedException] |
|
82 |
e = e.getCause |
|
83 |
} |
|
84 |
found_interrupt |
|
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 | 92 |
def expose() { if (Thread.interrupted) throw apply() } |
56861 | 93 |
def impose() { Thread.currentThread.interrupt } |
56860 | 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 | 118 |
/* message */ |
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 | 122 |
exn.getClass == classOf[User_Error]) |
59697
43e14b0e2ef8
more explicit exception User_Error, with value-oriented equality;
wenzelm
parents:
59138
diff
changeset
|
123 |
{ |
44158 | 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 | 126 |
} |
63782 | 127 |
else if (exn.isInstanceOf[java.sql.SQLException]) |
128 |
{ |
|
129 |
val msg = exn.getMessage |
|
130 |
Some(if (msg == null || msg == "") "SQL error" else msg) |
|
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 | 142 |
} |