src/Pure/GUI/gui.scala
changeset 65370 1324268c2f6a
parent 65083 9a0e34edfad1
child 67835 c8e4ee2b5482
equal deleted inserted replaced
65369:27c1b5e952bd 65370:1324268c2f6a
    91     text.editable = editable
    91     text.editable = editable
    92     new ScrollPane(text)
    92     new ScrollPane(text)
    93   }
    93   }
    94 
    94 
    95   private def simple_dialog(kind: Int, default_title: String,
    95   private def simple_dialog(kind: Int, default_title: String,
    96     parent: Component, title: String, message: Seq[Any])
    96     parent: Component, title: String, message: Iterable[Any])
    97   {
    97   {
    98     GUI_Thread.now {
    98     GUI_Thread.now {
    99       val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    99       val java_message =
   100       JOptionPane.showMessageDialog(parent,
   100         message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }).
   101         java_message.toArray.asInstanceOf[Array[AnyRef]],
   101           toArray.asInstanceOf[Array[AnyRef]]
       
   102       JOptionPane.showMessageDialog(parent, java_message,
   102         if (title == null) default_title else title, kind)
   103         if (title == null) default_title else title, kind)
   103     }
   104     }
   104   }
   105   }
   105 
   106 
   106   def dialog(parent: Component, title: String, message: Any*): Unit =
   107   def dialog(parent: Component, title: String, message: Any*): Unit =