src/Pure/Concurrent/future.ML
changeset 44247 270366301bd7
parent 44198 a41ea419de68
child 44249 64620f1d6f87
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
   471 fun get_result x =
   471 fun get_result x =
   472   (case peek x of
   472   (case peek x of
   473     NONE => Exn.Exn (Fail "Unfinished future")
   473     NONE => Exn.Exn (Fail "Unfinished future")
   474   | SOME res =>
   474   | SOME res =>
   475       if Exn.is_interrupt_exn res then
   475       if Exn.is_interrupt_exn res then
   476         (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of
   476         (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
   477           [] => res
   477           NONE => res
   478         | exns => Exn.Exn (Exn.EXCEPTIONS exns))
   478         | SOME exn => Exn.Exn exn)
   479       else res);
   479       else res);
   480 
   480 
   481 fun join_next deps = (*requires SYNCHRONIZED*)
   481 fun join_next deps = (*requires SYNCHRONIZED*)
   482   if null deps then NONE
   482   if null deps then NONE
   483   else
   483   else