# HG changeset patch
# User wenzelm
# Date 1296512503 -3600
# Node ID 4639f40b20c9b5f073fb3aaa1b440d221d40a573
# Parent  0f0f6212d6c6f2f9fc8917b527bbc058e4df71b9
name "passive" tasks (practically lazy values);

diff -r 0f0f6212d6c6 -r 4639f40b20c9 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 23:10:16 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 23:21:43 2011 +0100
@@ -225,7 +225,7 @@
 
 fun enqueue_passive group abort (Queue {groups, jobs}) =
   let
-    val task = new_task "" NONE;
+    val task = new_task "passive" NONE;
     val groups' = groups
       |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
     val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive abort));