# HG changeset patch
# User wenzelm
# Date 1274470111 -7200
# Node ID 78d88b670a53e74f5a3fefd330b4418e5432e557
# Parent  83ea8b551280c9939762c5b4f7ad9c1334bdbe11
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);

diff -r 83ea8b551280 -r 78d88b670a53 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri May 21 20:46:00 2010 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri May 21 21:28:31 2010 +0200
@@ -170,12 +170,14 @@
 fun future_job group (e: unit -> 'a) =
   let
     val result = Single_Assignment.var "future" : 'a result;
+    val pos = Position.thread_data ();
     fun job ok =
       let
         val res =
           if ok then
             Exn.capture (fn () =>
-              Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) ()
+              Multithreading.with_attributes Multithreading.private_interrupts
+                (fn _ => Position.setmp_thread_data pos e ())) ()
           else Exn.Exn Exn.Interrupt;
       in assign_result group result res end;
   in (result, job) end;