diff -r 27c1b5e952bd -r 1324268c2f6a src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Tue Apr 04 17:14:41 2017 +0200 +++ b/src/Pure/GUI/gui.scala Tue Apr 04 18:43:47 2017 +0200 @@ -93,12 +93,13 @@ } private def simple_dialog(kind: Int, default_title: String, - parent: Component, title: String, message: Seq[Any]) + parent: Component, title: String, message: Iterable[Any]) { GUI_Thread.now { - val java_message = message map { case x: scala.swing.Component => x.peer case x => x } - JOptionPane.showMessageDialog(parent, - java_message.toArray.asInstanceOf[Array[AnyRef]], + val java_message = + message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }). + toArray.asInstanceOf[Array[AnyRef]] + JOptionPane.showMessageDialog(parent, java_message, if (title == null) default_title else title, kind) } }