equal
deleted
inserted
replaced
436 |
436 |
437 fun error_msg pos ((serial, msg), exec_id) = |
437 fun error_msg pos ((serial, msg), exec_id) = |
438 Position.setmp_thread_data pos (fn () => |
438 Position.setmp_thread_data pos (fn () => |
439 let val id = Position.get_id pos in |
439 let val id = Position.get_id pos in |
440 if is_none id orelse is_none exec_id orelse id = exec_id |
440 if is_none id orelse is_none exec_id orelse id = exec_id |
441 then Output.error_msg' (serial, msg) else () |
441 then Output.error_message' (serial, msg) else () |
442 end) (); |
442 end) (); |
443 |
443 |
444 fun identify_result pos res = |
444 fun identify_result pos res = |
445 (case res of |
445 (case res of |
446 Exn.Exn exn => |
446 Exn.Exn exn => |