src/Pure/Concurrent/future.ML
changeset 50931 a7484a7b6c8a
parent 50916 fd902b616b48
child 50974 55f8bd61b029
equal deleted inserted replaced
50930:23601c59f347 50931:a7484a7b6c8a
   437 
   437 
   438 (* results *)
   438 (* results *)
   439 
   439 
   440 fun error_msg pos ((serial, msg), exec_id) =
   440 fun error_msg pos ((serial, msg), exec_id) =
   441   Position.setmp_thread_data pos (fn () =>
   441   Position.setmp_thread_data pos (fn () =>
   442     if is_none exec_id orelse exec_id = Position.get_id pos
   442     let val id = Position.get_id pos in
   443     then Output.error_msg' (serial, msg) else warning msg) ();
   443       if is_none id orelse is_none exec_id orelse id = exec_id
       
   444       then Output.error_msg' (serial, msg) else ()
       
   445     end) ();
   444 
   446 
   445 fun identify_result pos res =
   447 fun identify_result pos res =
   446   (case res of
   448   (case res of
   447     Exn.Exn exn =>
   449     Exn.Exn exn =>
   448       let val exec_id =
   450       let val exec_id =