--- a/Admin/lib/Tools/components_checksum Thu Jan 17 14:06:14 2013 +0100
+++ b/Admin/lib/Tools/components_checksum Thu Jan 17 14:12:35 2013 +0100
@@ -71,11 +71,10 @@
(
cd "$COMPONENTS_DIR"
- sha1sum *.tar.gz > "$CHECKSUM_TMP"
+ sha1sum *.tar.gz | sort -k2 > "$CHECKSUM_TMP"
)
[ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
[ -n "$CHECK" ] && {
diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error"
}
-
--- a/src/Pure/Concurrent/future.ML Thu Jan 17 14:06:14 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Jan 17 14:12:35 2013 +0100
@@ -439,8 +439,10 @@
fun error_msg pos ((serial, msg), exec_id) =
Position.setmp_thread_data pos (fn () =>
- if is_none exec_id orelse exec_id = Position.get_id pos
- then Output.error_msg' (serial, msg) else warning msg) ();
+ let val id = Position.get_id pos in
+ if is_none id orelse is_none exec_id orelse id = exec_id
+ then Output.error_msg' (serial, msg) else ()
+ end) ();
fun identify_result pos res =
(case res of
--- a/src/Pure/Tools/build_dialog.scala Thu Jan 17 14:06:14 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala Thu Jan 17 14:12:35 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()
}
})
}