--- a/src/Pure/General/exn.scala Wed May 09 20:45:57 2018 +0200
+++ b/src/Pure/General/exn.scala Wed May 09 22:03:02 2018 +0200
@@ -31,13 +31,11 @@
def error(message: String): Nothing = throw ERROR(message)
- def cat_message(msg1: String, msg2: String): String =
- if (msg1 == "") msg2
- else if (msg2 == "") msg1
- else msg1 + "\n" + msg2
+ def cat_message(msgs: String*): String =
+ cat_lines(msgs.iterator.filterNot(_ == ""))
- def cat_error(msg1: String, msg2: String): Nothing =
- error(cat_message(msg1, msg2))
+ def cat_error(msgs: String*): Nothing =
+ error(cat_message(msgs:_*))
/* exceptions as values */
--- a/src/Pure/ROOT.scala Wed May 09 20:45:57 2018 +0200
+++ b/src/Pure/ROOT.scala Wed May 09 22:03:02 2018 +0200
@@ -8,7 +8,7 @@
{
val ERROR = Exn.ERROR
val error = Exn.error _
- val cat_error = Exn.cat_error _
+ def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*)
def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(f)
val space_explode = Library.space_explode _