# HG changeset patch
# User wenzelm
# Date 1358420645 -3600
# Node ID 23601c59f347aab5559717cecd352300c22a7190
# Parent  b1939139f8f36ab52aec9f9f690a4c126bf2049c
delay to give users a chance to see what was happening, even with auto_close enabled;

diff -r b1939139f8f3 -r 23601c59f347 src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Thu Jan 17 10:44:51 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Thu Jan 17 12:04:05 2013 +0100
@@ -120,13 +120,15 @@
     val button = new Button("Cancel") {
       reactions += { case ButtonClicked(_) => button_action() }
     }
-    def button_exit()
-    {
-      check_auto_close()
-      button.text = if (return_code == 0) "OK" else "Exit"
-      button_action = (() => sys.exit(return_code))
-      button.peer.getRootPane.setDefaultButton(button.peer)
-    }
+
+    val delay_button_exit =
+      Swing_Thread.delay_first(Time.seconds(1.0))
+      {
+        check_auto_close()
+        button.text = if (return_code == 0) "OK" else "Exit"
+        button_action = (() => sys.exit(return_code))
+        button.peer.getRootPane.setDefaultButton(button.peer)
+      }
 
 
     val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button, auto_close)
@@ -157,7 +159,7 @@
       Swing_Thread.now {
         progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
         return_code = rc
-        button_exit()
+        delay_button_exit.invoke()
       }
     })
   }