# HG changeset patch # User wenzelm # Date 1358368783 -3600 # Node ID fd902b616b4869824c11f6cd7b825f2c590a2593 # Parent 12de8ea66f54b707d46b0711f8e9d5cd1c63490b proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document; diff -r 12de8ea66f54 -r fd902b616b48 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