# HG changeset patch
# User wenzelm
# Date 1378555632 -7200
# Node ID 1a0c39c728a171f0cb254677f413624bc54cc91a
# Parent  20ff79162ff3812ac78d27b2698aa87b7ceffded
clarified result;

diff -r 20ff79162ff3 -r 1a0c39c728a1 src/Pure/System/system_dialog.scala
--- a/src/Pure/System/system_dialog.scala	Sat Sep 07 13:59:47 2013 +0200
+++ b/src/Pure/System/system_dialog.scala	Sat Sep 07 14:07:12 2013 +0200
@@ -14,8 +14,11 @@
 import scala.swing.event.ButtonClicked
 
 
-class System_Dialog(continue: Int => Unit) extends Build.Progress
+class System_Dialog extends Build.Progress
 {
+  val result = Future.promise[Int]
+
+
   /* GUI state -- owned by Swing thread */
 
   private var _title = "Isabelle"
@@ -42,10 +45,11 @@
       }
   }
 
-  def conclude()
+  private def conclude()
   {
     Swing_Thread.require()
     require(_return_code.isDefined)
+    require(!result.is_finished)
 
     _window match {
       case None =>
@@ -54,7 +58,7 @@
         _window = None
     }
 
-    continue(_return_code.get)
+    result.fulfill(_return_code.get)
   }