equal
deleted
inserted
replaced
29 def unapply(exn: Throwable): Option[String] = user_message(exn) |
29 def unapply(exn: Throwable): Option[String] = user_message(exn) |
30 } |
30 } |
31 |
31 |
32 def error(message: String): Nothing = throw ERROR(message) |
32 def error(message: String): Nothing = throw ERROR(message) |
33 |
33 |
34 def cat_message(msg1: String, msg2: String): String = |
34 def cat_message(msgs: String*): String = |
35 if (msg1 == "") msg2 |
35 cat_lines(msgs.iterator.filterNot(_ == "")) |
36 else if (msg2 == "") msg1 |
|
37 else msg1 + "\n" + msg2 |
|
38 |
36 |
39 def cat_error(msg1: String, msg2: String): Nothing = |
37 def cat_error(msgs: String*): Nothing = |
40 error(cat_message(msg1, msg2)) |
38 error(cat_message(msgs:_*)) |
41 |
39 |
42 |
40 |
43 /* exceptions as values */ |
41 /* exceptions as values */ |
44 |
42 |
45 sealed abstract class Result[A] |
43 sealed abstract class Result[A] |