src/Pure/Concurrent/task_queue.ML

 
 
 (* queue *)
 
 datatype queue = Queue of
- {groups: task list Inttab.table,   (*groups with presently active members*)
+ {groups: task list Inttab.table,   (*groups with presently known members*)
   jobs: jobs};                      (*job dependency graph*)
 
 fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
 
 val empty = make_queue Inttab.empty Task_Graph.empty;