# HG changeset patch
# User wenzelm
# Date 1262299629 -3600
# Node ID ada8eb23a08ea71836b0e6eff318ce1ba61ed10e
# Parent  f0322b5951469cd6371e10a4bbd274d97b12c6cd
added simple dialogs;

diff -r f0322b595146 -r ada8eb23a08e 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) =