author | wenzelm |
Wed, 23 Apr 2014 12:39:23 +0200 | |
changeset 56667 | 65e84b0ef974 |
parent 52066 | 83b7b88770c9 |
child 56670 | 3f23441453d0 |
permissions | -rw-r--r-- |
34136 | 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 |
{ |
|
44158 | 13 |
/* exceptions as values */ |
34136 | 14 |
|
15 |
sealed abstract class Result[A] |
|
43762 | 16 |
case class Res[A](res: A) extends Result[A] |
17 |
case class Exn[A](exn: Throwable) extends Result[A] |
|
34136 | 18 |
|
19 |
def capture[A](e: => A): Result[A] = |
|
20 |
try { Res(e) } |
|
34313
2f890016afab
treat *all* JVM throwables as "exceptions", cf. ML version;
wenzelm
parents:
34300
diff
changeset
|
21 |
catch { case exn: Throwable => Exn[A](exn) } |
34136 | 22 |
|
23 |
def release[A](result: Result[A]): A = |
|
24 |
result match { |
|
25 |
case Res(x) => x |
|
26 |
case Exn(exn) => throw exn |
|
27 |
} |
|
44158 | 28 |
|
29 |
||
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
30 |
/* interrupts */ |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
31 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
32 |
def is_interrupt(exn: Throwable): Boolean = |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
33 |
exn.isInstanceOf[InterruptedException] |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
34 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
35 |
object Interrupt |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
36 |
{ |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
37 |
def apply(): Throwable = new InterruptedException |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
38 |
def unapply(exn: Throwable): Boolean = is_interrupt(exn) |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
39 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
40 |
val return_code = 130 |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
41 |
} |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
42 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
43 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
44 |
/* POSIX return code */ |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
45 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
46 |
def return_code(exn: Throwable, rc: Int): Int = |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
47 |
if (is_interrupt(exn)) Interrupt.return_code else rc |
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
48 |
|
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
49 |
|
44158 | 50 |
/* message */ |
51 |
||
52 |
private val runtime_exception = Class.forName("java.lang.RuntimeException") |
|
53 |
||
48479
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
54 |
def user_message(exn: Throwable): Option[String] = |
48476 | 55 |
if (exn.isInstanceOf[java.io.IOException]) { |
56 |
val msg = exn.getMessage |
|
48479
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
57 |
Some(if (msg == null) "I/O error" else "I/O error: " + msg) |
48476 | 58 |
} |
59 |
else if (exn.getClass == runtime_exception) { |
|
44158 | 60 |
val msg = exn.getMessage |
48479
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
61 |
Some(if (msg == null) "Error" else msg) |
44158 | 62 |
} |
48479
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
63 |
else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString) |
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
64 |
else None |
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
65 |
|
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48476
diff
changeset
|
66 |
def message(exn: Throwable): String = |
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
52066
diff
changeset
|
67 |
user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString) |
34136 | 68 |
} |
69 |