equal
deleted
inserted
replaced
74 /* simple dialogs */ |
74 /* simple dialogs */ |
75 |
75 |
76 private def simple_dialog(kind: Int, default_title: String) |
76 private def simple_dialog(kind: Int, default_title: String) |
77 (parent: Component, title: String, message: Any*) |
77 (parent: Component, title: String, message: Any*) |
78 { |
78 { |
79 JOptionPane.showMessageDialog(parent, |
79 Swing_Thread.now { |
80 message.toArray.asInstanceOf[Array[AnyRef]], |
80 JOptionPane.showMessageDialog(parent, |
81 if (title == null) default_title else title, kind) |
81 message.toArray.asInstanceOf[Array[AnyRef]], |
|
82 if (title == null) default_title else title, kind) |
|
83 } |
82 } |
84 } |
83 |
85 |
84 def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _ |
86 def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _ |
85 def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _ |
87 def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _ |
86 def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _ |
88 def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _ |