# HG changeset patch
# User wenzelm
# Date 1289333586 -3600
# Node ID f9347a30d1b2abf30e292a471d2c1776110a9e81
# Parent  7434faac7e21199c8b573f5b5b056f9f140eb690
explicitly identify forked/joined tasks;

diff -r 7434faac7e21 -r f9347a30d1b2 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;