equal
deleted
inserted
replaced
407 local |
407 local |
408 |
408 |
409 fun get_result x = |
409 fun get_result x = |
410 (case peek x of |
410 (case peek x of |
411 NONE => Exn.Exn (SYS_ERROR "unfinished future") |
411 NONE => Exn.Exn (SYS_ERROR "unfinished future") |
412 | SOME (Exn.Exn Exn.Interrupt) => |
412 | SOME (exn as Exn.Exn Exn.Interrupt) => |
413 Exn.Exn (Exn.EXCEPTIONS (Exn.flatten_list (Task_Queue.group_status (group_of x)))) |
413 (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of |
|
414 [] => exn |
|
415 | exns => Exn.Exn (Exn.EXCEPTIONS exns)) |
414 | SOME res => res); |
416 | SOME res => res); |
415 |
417 |
416 fun join_next deps = (*requires SYNCHRONIZED*) |
418 fun join_next deps = (*requires SYNCHRONIZED*) |
417 if null deps then NONE |
419 if null deps then NONE |
418 else |
420 else |