--- a/src/Pure/Concurrent/future.ML Fri May 28 22:51:04 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Sat May 29 15:31:15 2010 +0200
@@ -409,8 +409,10 @@
fun get_result x =
(case peek x of
NONE => Exn.Exn (SYS_ERROR "unfinished future")
- | SOME (Exn.Exn Exn.Interrupt) =>
- Exn.Exn (Exn.EXCEPTIONS (Exn.flatten_list (Task_Queue.group_status (group_of x))))
+ | SOME (exn as Exn.Exn Exn.Interrupt) =>
+ (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
+ [] => exn
+ | exns => Exn.Exn (Exn.EXCEPTIONS exns))
| SOME res => res);
fun join_next deps = (*requires SYNCHRONIZED*)