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