equal
deleted
inserted
replaced
437 |
437 |
438 fun assign_result group result raw_res = |
438 fun assign_result group result raw_res = |
439 let |
439 let |
440 val res = |
440 val res = |
441 (case raw_res of |
441 (case raw_res of |
442 Exn.Exn exn => Exn.Exn (Par_Exn.set_serial exn) |
442 Exn.Exn exn => Exn.Exn (Par_Exn.identify [] exn) |
443 | _ => raw_res); |
443 | _ => raw_res); |
444 val _ = Single_Assignment.assign result res |
444 val _ = Single_Assignment.assign result res |
445 handle exn as Fail _ => |
445 handle exn as Fail _ => |
446 (case Single_Assignment.peek result of |
446 (case Single_Assignment.peek result of |
447 SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn) |
447 SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn) |