tuned;
authorwenzelm
Thu Jul 24 11:46:40 2014 +0200 (2014-07-24)
changeset 57639ba170c8ea578
parent 57638 ed58e740a699
child 57640 0a28cf866d5d
tuned;
src/Pure/GUI/gui.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Thu Jul 24 10:38:46 2014 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Thu Jul 24 11:46:40 2014 +0200
     1.3 @@ -97,13 +97,13 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def dialog(parent: Component, title: String, message: Any*) =
     1.8 +  def dialog(parent: Component, title: String, message: Any*): Unit =
     1.9      simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
    1.10  
    1.11 -  def warning_dialog(parent: Component, title: String, message: Any*) =
    1.12 +  def warning_dialog(parent: Component, title: String, message: Any*): Unit =
    1.13      simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
    1.14  
    1.15 -  def error_dialog(parent: Component, title: String, message: Any*) =
    1.16 +  def error_dialog(parent: Component, title: String, message: Any*): Unit =
    1.17      simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
    1.18  
    1.19    def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =