src/Pure/System/system_dialog.scala

--- a/src/Pure/System/system_dialog.scala	Sat Sep 07 14:14:25 2013 +0200
+++ b/src/Pure/System/system_dialog.scala	Sat Sep 07 15:10:33 2013 +0200
@@ -17,9 +17,6 @@
 
 class System_Dialog extends Build.Progress
 {
-  val result = Future.promise[Int]
-
-
   /* GUI state -- owned by Swing thread */
 
   private var _title = "Isabelle"
@@ -46,11 +43,12 @@
       }
   }
 
+  private val result = Future.promise[Int]
+
   private def conclude()
   {
     Swing_Thread.require()
     require(_return_code.isDefined)
-    require(!result.is_finished)
 
     _window match {
       case None =>
@@ -59,9 +57,12 @@
         _window = None
     }
 
-    result.fulfill(_return_code.get)
+    try { result.fulfill(_return_code.get) }
+    catch { case ERROR(_) => }
   }
 
+  def join(): Int = result.join
+
 
   /* window */
 
@@ -164,7 +165,10 @@
   def return_code(rc: Int): Unit =
     Swing_Thread.later {
       _return_code = Some(rc)
-      _window.foreach(window => window.delay_exit.invoke)
+      _window match {
+        case None => conclude()
+        case Some(window) => window.delay_exit.invoke
+      }
     }
 
   override def echo(txt: String): Unit =