equal
deleted
inserted
replaced
4 Toplevel isabelle package. |
4 Toplevel isabelle package. |
5 */ |
5 */ |
6 |
6 |
7 package object isabelle |
7 package object isabelle |
8 { |
8 { |
|
9 /* errors */ |
|
10 |
9 object ERROR |
11 object ERROR |
10 { |
12 { |
11 def apply(message: String): Throwable = new RuntimeException(message) |
13 def apply(message: String): Throwable = new RuntimeException(message) |
12 def unapply(exn: Throwable): Option[String] = |
14 def unapply(exn: Throwable): Option[String] = |
13 exn match { |
15 exn match { |
15 val msg = e.getMessage |
17 val msg = e.getMessage |
16 Some(if (msg == null) "" else msg) |
18 Some(if (msg == null) "" else msg) |
17 case _ => None |
19 case _ => None |
18 } |
20 } |
19 } |
21 } |
|
22 |
20 def error(message: String): Nothing = throw ERROR(message) |
23 def error(message: String): Nothing = throw ERROR(message) |
|
24 |
|
25 def cat_error(msg1: String, msg2: String): Nothing = |
|
26 if (msg1 == "") error(msg1) |
|
27 else error(msg1 + "\n" + msg2) |
21 } |
28 } |
22 |
29 |