src/Pure/Concurrent/future.ML
changeset 50911 ee7fe4230642
parent 50909 b2fb1ab1475d
child 50914 fe4714886d92
equal deleted inserted replaced
50910:54f06ba192ef 50911:ee7fe4230642
   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)