# HG changeset patch
# User wenzelm
# Date 1525896182 -7200
# Node ID 62a3294edda36d8c41047c3e1916cbc3f61fb162
# Parent  6fb85346cb7966c44be2df37942995bb275c34c0
tuned signature;

diff -r 6fb85346cb79 -r 62a3294edda3 src/Pure/General/exn.scala
--- 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 */
diff -r 6fb85346cb79 -r 62a3294edda3 src/Pure/ROOT.scala
--- 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 _