tuned;
authorwenzelm
Tue Apr 04 18:43:47 2017 +0200 (2017-04-04 ago)
changeset 653731324268c2f6a
parent 65372 27c1b5e952bd
child 65374 ce09e947c1d5
tuned;
src/Pure/GUI/gui.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Tue Apr 04 17:14:41 2017 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Tue Apr 04 18:43:47 2017 +0200
     1.3 @@ -93,12 +93,13 @@
     1.4    }
     1.5  
     1.6    private def simple_dialog(kind: Int, default_title: String,
     1.7 -    parent: Component, title: String, message: Seq[Any])
     1.8 +    parent: Component, title: String, message: Iterable[Any])
     1.9    {
    1.10      GUI_Thread.now {
    1.11 -      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    1.12 -      JOptionPane.showMessageDialog(parent,
    1.13 -        java_message.toArray.asInstanceOf[Array[AnyRef]],
    1.14 +      val java_message =
    1.15 +        message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }).
    1.16 +          toArray.asInstanceOf[Array[AnyRef]]
    1.17 +      JOptionPane.showMessageDialog(parent, java_message,
    1.18          if (title == null) default_title else title, kind)
    1.19      }
    1.20    }