proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
1.1 --- a/src/Pure/Concurrent/future.ML Wed Jan 16 21:09:29 2013 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Wed Jan 16 21:39:43 2013 +0100
1.3 @@ -438,8 +438,9 @@
1.4 (* results *)
1.5
1.6 fun error_msg pos ((serial, msg), exec_id) =
1.7 - if is_none exec_id orelse exec_id = Position.get_id pos
1.8 - then Output.error_msg' (serial, msg) else warning msg;
1.9 + Position.setmp_thread_data pos (fn () =>
1.10 + if is_none exec_id orelse exec_id = Position.get_id pos
1.11 + then Output.error_msg' (serial, msg) else warning msg) ();
1.12
1.13 fun identify_result pos res =
1.14 (case res of