1 /* Title: Pure/RAW/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 /* 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 |
|
44 /* exceptions as values */ |
|
45 |
|
46 sealed abstract class Result[A] |
|
47 { |
|
48 def user_error: Result[A] = |
|
49 this match { |
|
50 case Exn(ERROR(msg)) => Exn(ERROR(msg)) |
|
51 case _ => this |
|
52 } |
|
53 } |
|
54 case class Res[A](res: A) extends Result[A] |
|
55 case class Exn[A](exn: Throwable) extends Result[A] |
|
56 |
|
57 def capture[A](e: => A): Result[A] = |
|
58 try { Res(e) } |
|
59 catch { case exn: Throwable => Exn[A](exn) } |
|
60 |
|
61 def release[A](result: Result[A]): A = |
|
62 result match { |
|
63 case Res(x) => x |
|
64 case Exn(exn) => throw exn |
|
65 } |
|
66 |
|
67 def release_first[A](results: List[Result[A]]): List[A] = |
|
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 } |
|
72 |
|
73 |
|
74 /* interrupts */ |
|
75 |
|
76 def is_interrupt(exn: Throwable): Boolean = |
|
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 } |
|
86 |
|
87 object Interrupt |
|
88 { |
|
89 def apply(): Throwable = new InterruptedException |
|
90 def unapply(exn: Throwable): Boolean = is_interrupt(exn) |
|
91 |
|
92 def expose() { if (Thread.interrupted) throw apply() } |
|
93 def impose() { Thread.currentThread.interrupt } |
|
94 |
|
95 def postpone[A](body: => A): Option[A] = |
|
96 { |
|
97 val interrupted = Thread.interrupted |
|
98 val result = capture { body } |
|
99 if (interrupted) impose() |
|
100 result match { |
|
101 case Res(x) => Some(x) |
|
102 case Exn(e) => |
|
103 if (is_interrupt(e)) { impose(); None } |
|
104 else throw e |
|
105 } |
|
106 } |
|
107 |
|
108 val return_code = 130 |
|
109 } |
|
110 |
|
111 |
|
112 /* POSIX return code */ |
|
113 |
|
114 def return_code(exn: Throwable, rc: Int): Int = |
|
115 if (is_interrupt(exn)) Interrupt.return_code else rc |
|
116 |
|
117 |
|
118 /* message */ |
|
119 |
|
120 def user_message(exn: Throwable): Option[String] = |
|
121 if (exn.getClass == classOf[RuntimeException] || |
|
122 exn.getClass == classOf[User_Error]) |
|
123 { |
|
124 val msg = exn.getMessage |
|
125 Some(if (msg == null || msg == "") "Error" else msg) |
|
126 } |
|
127 else if (exn.isInstanceOf[java.io.IOException]) |
|
128 { |
|
129 val msg = exn.getMessage |
|
130 Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg) |
|
131 } |
|
132 else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString) |
|
133 else None |
|
134 |
|
135 def message(exn: Throwable): String = |
|
136 user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString) |
|
137 } |
|