added simple dialogs;
authorwenzelm
Thu, 31 Dec 2009 23:47:09 +0100
changeset 34216 ada8eb23a08e
parent 34215 f0322b595146
child 34217 67e1ac2d3b2c
child 34221 3ae38d4b090c
child 34234 86a985e9b4df
added simple dialogs;
src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Dec 31 00:35:54 2009 +0100
+++ b/src/Pure/library.scala	Thu Dec 31 23:47:09 2009 +0100
@@ -7,6 +7,8 @@
 package isabelle
 
 import java.lang.System
+import java.awt.Component
+import javax.swing.JOptionPane
 
 
 object Library
@@ -36,6 +38,21 @@
   }
 
 
+  /* simple dialogs */
+
+  private def simple_dialog(kind: Int, default_title: String)
+    (parent: Component, title: String, message: Any*)
+  {
+    JOptionPane.showMessageDialog(parent,
+      message.toArray.asInstanceOf[Array[AnyRef]],
+      if (title == null) default_title else title, kind)
+  }
+
+  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
+  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
+  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
+
+
   /* timing */
 
   def timeit[A](e: => A) =