clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
authorwenzelm
Thu, 17 Jan 2013 12:04:52 +0100
changeset 50931 a7484a7b6c8a
parent 50930 23601c59f347
child 50932 ca071373b695
clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jan 17 12:04:05 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Jan 17 12:04:52 2013 +0100
@@ -439,8 +439,10 @@
 
 fun error_msg pos ((serial, msg), exec_id) =
   Position.setmp_thread_data pos (fn () =>
-    if is_none exec_id orelse exec_id = Position.get_id pos
-    then Output.error_msg' (serial, msg) else warning msg) ();
+    let val id = Position.get_id pos in
+      if is_none id orelse is_none exec_id orelse id = exec_id
+      then Output.error_msg' (serial, msg) else ()
+    end) ();
 
 fun identify_result pos res =
   (case res of