added simple dialogs;
authorwenzelm
Thu, 31 Dec 2009 23:47:09 +0100
changeset 34216ada8eb23a08e
parent 34215 f0322b595146
child 34217 3ae38d4b090c
child 34220 67e1ac2d3b2c
child 34234 86a985e9b4df
added simple dialogs;
src/Pure/library.scala
     1.1 --- a/src/Pure/library.scala	Thu Dec 31 00:35:54 2009 +0100
     1.2 +++ b/src/Pure/library.scala	Thu Dec 31 23:47:09 2009 +0100
     1.3 @@ -7,6 +7,8 @@
     1.4  package isabelle
     1.5  
     1.6  import java.lang.System
     1.7 +import java.awt.Component
     1.8 +import javax.swing.JOptionPane
     1.9  
    1.10  
    1.11  object Library
    1.12 @@ -36,6 +38,21 @@
    1.13    }
    1.14  
    1.15  
    1.16 +  /* simple dialogs */
    1.17 +
    1.18 +  private def simple_dialog(kind: Int, default_title: String)
    1.19 +    (parent: Component, title: String, message: Any*)
    1.20 +  {
    1.21 +    JOptionPane.showMessageDialog(parent,
    1.22 +      message.toArray.asInstanceOf[Array[AnyRef]],
    1.23 +      if (title == null) default_title else title, kind)
    1.24 +  }
    1.25 +
    1.26 +  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
    1.27 +  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
    1.28 +  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
    1.29 +
    1.30 +
    1.31    /* timing */
    1.32  
    1.33    def timeit[A](e: => A) =