src/Pure/Concurrent/future.ML
changeset 44249 64620f1d6f87
parent 44247 270366301bd7
child 44268 f6a11c1da821
equal deleted inserted replaced
44248:6a3541412b23 44249:64620f1d6f87
   392 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
   392 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
   393 
   393 
   394 
   394 
   395 (* future jobs *)
   395 (* future jobs *)
   396 
   396 
   397 fun assign_result group result res =
   397 fun assign_result group result raw_res =
   398   let
   398   let
       
   399     val res =
       
   400       (case raw_res of
       
   401         Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
       
   402       | _ => raw_res);
   399     val _ = Single_Assignment.assign result res
   403     val _ = Single_Assignment.assign result res
   400       handle exn as Fail _ =>
   404       handle exn as Fail _ =>
   401         (case Single_Assignment.peek result of
   405         (case Single_Assignment.peek result of
   402           SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
   406           SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
   403         | _ => reraise exn);
   407         | _ => reraise exn);