# HG changeset patch
# User wenzelm
# Date 1222597425 -7200
# Node ID 0b9fb63b8e1d6511893dd893a7ac8cfc88576df5
# Parent  777bdc429ea382d6a49eb13c1067a16f0de9cca5
proper setmp_thread_data for nested execute (cf. join_loop);

diff -r 777bdc429ea3 -r 0b9fb63b8e1d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sun Sep 28 12:23:44 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Sep 28 12:23:45 2008 +0200
@@ -58,7 +58,7 @@
 
 local val tag = Universal.tag () : (string * task * group) option Universal.tag in
   fun thread_data () = the_default NONE (Thread.getLocal tag);
-  fun set_thread_data x = Thread.setLocal (tag, x);
+  fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
 end;
 
 
@@ -135,11 +135,9 @@
 fun execute name (task, group, run) =
   let
     val _ = trace_active ();
-    val _ = set_thread_data (SOME (name, task, group));
     val _ = Multithreading.tracing 3 (fn () => name ^ ": running");
-    val ok = run ();
+    val ok = setmp_thread_data (name, task, group) run ();
     val _ = Multithreading.tracing 3 (fn () => name ^ ": finished");
-    val _ = set_thread_data NONE;
     val _ = SYNCHRONIZED "execute" (fn () =>
      (change queue (TaskQueue.finish task);
       if ok then ()