proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
authorwenzelm
Wed, 16 Jan 2013 21:39:43 +0100
changeset 50916 fd902b616b48
parent 50915 12de8ea66f54
child 50917 9459f59cff09
proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jan 16 21:09:29 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Jan 16 21:39:43 2013 +0100
@@ -438,8 +438,9 @@
 (* results *)
 
 fun error_msg pos ((serial, msg), exec_id) =
-  if is_none exec_id orelse exec_id = Position.get_id pos
-  then Output.error_msg' (serial, msg) else warning msg;
+  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) ();
 
 fun identify_result pos res =
   (case res of