equal
deleted
inserted
replaced
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 = |