equal
deleted
inserted
replaced
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); |