explicitly identify forked/joined tasks;
authorwenzelm
Tue, 09 Nov 2010 21:13:06 +0100
changeset 40448 f9347a30d1b2
parent 40447 7434faac7e21
child 40449 9c390868d255
explicitly identify forked/joined tasks;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Nov 09 11:27:58 2010 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Nov 09 21:13:06 2010 +0100
@@ -552,9 +552,13 @@
 
 fun status e =
   let
-    val _ = Output.status (Markup.markup Markup.forked "");
+    val task_props =
+      (case worker_task () of
+        NONE => I
+      | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
+    val _ = Output.status (Markup.markup (task_props Markup.forked) "");
     val x = e ();  (*sic -- report "joined" only for success*)
-    val _ = Output.status (Markup.markup Markup.joined "");
+    val _ = Output.status (Markup.markup (task_props Markup.joined) "");
   in x end;