src/Pure/Concurrent/task_queue.ML
author wenzelm
Thu, 11 Sep 2008 18:07:58 +0200
changeset 28202 23cb9a974630
parent 28196 f019dd2db561
child 28204 2d93b158ad99
permissions -rw-r--r--
added focus, which indicates a particular collection of high-priority tasks; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/task_queue.ML
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     4
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     5
Ordered queue of grouped tasks.
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     6
*)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     7
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     8
signature TASK_QUEUE =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     9
sig
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    10
  eqtype task
28196
wenzelm
parents: 28190
diff changeset
    11
  val str_of_task: task -> string
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    12
  eqtype group
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    13
  val new_group: unit -> group
28179
8e8313aededc human-readable printing of TaskQueue.task/group;
wenzelm
parents: 28176
diff changeset
    14
  val str_of_group: group -> string
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    15
  type queue
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    16
  val empty: queue
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    17
  val enqueue: group -> task list -> (bool -> bool) -> queue -> task * queue
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    18
  val depend: task list -> task -> queue -> queue
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    19
  val focus: task list -> queue -> queue
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    20
  val dequeue: queue -> (task * group * (unit -> bool)) option * queue
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    21
  val dequeue_towards: task list -> queue -> (task * group * (unit -> bool)) option * queue
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    22
  val interrupt: queue -> task -> unit
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    23
  val interrupt_external: queue -> string -> unit
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    24
  val finish: task -> queue -> queue
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    25
  val cancel: queue -> group -> bool
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    26
end;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    27
28171
9b2f9cc9ff4b proper signature constraint;
wenzelm
parents: 28168
diff changeset
    28
structure TaskQueue: TASK_QUEUE =
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    29
struct
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    30
28168
ba410235ff04 moved thread data to future.ML (again);
wenzelm
parents: 28165
diff changeset
    31
(* identifiers *)
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    32
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    33
datatype task = Task of serial;
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    34
fun str_of_task (Task i) = string_of_int i;
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    35
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    36
datatype group = Group of serial * bool ref;
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    37
fun new_group () = Group (serial (), ref true);
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    38
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    39
fun str_of_group (Group (i, ref ok)) =
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    40
  if ok then string_of_int i else enclose "(" ")" (string_of_int i);
28179
8e8313aededc human-readable printing of TaskQueue.task/group;
wenzelm
parents: 28176
diff changeset
    41
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    42
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    43
(* jobs *)
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    44
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    45
datatype job =
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    46
  Job of bool -> bool |
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    47
  Running of Thread.thread;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    48
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    49
type jobs = (group * job) IntGraph.T;
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    50
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    51
fun get_group (jobs: jobs) (Task id) = #1 (IntGraph.get_node jobs id);
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    52
fun get_job (jobs: jobs) (Task id) = #2 (IntGraph.get_node jobs id);
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    53
fun map_job (Task id) f (jobs: jobs) = IntGraph.map_node id (apsnd f) jobs;
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    54
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    55
fun add_job (Task id) (Task dep) (jobs: jobs) =
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    56
  IntGraph.add_edge_acyclic (dep, id) jobs handle IntGraph.UNDEF _ => jobs;
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    57
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    58
fun check_job (jobs: jobs) (task as Task id) =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    59
  if can (IntGraph.get_node jobs) id then SOME task else NONE;
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    60
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    61
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    62
(* queue of grouped jobs *)
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    63
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    64
datatype queue = Queue of
28184
5ed5cb73a2e9 eliminated cache, access queue efficiently via IntGraph.get_first;
wenzelm
parents: 28179
diff changeset
    65
 {groups: task list Inttab.table,   (*groups with presently active members*)
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    66
  jobs: jobs,                       (*job dependency graph*)
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    67
  focus: task list};                (*particular collection of high-priority tasks*)
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    68
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    69
fun make_queue groups jobs focus = Queue {groups = groups, jobs = jobs, focus = focus};
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    70
val empty = make_queue Inttab.empty IntGraph.empty [];
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    71
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    72
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    73
(* enqueue *)
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    74
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    75
fun enqueue (group as Group (gid, _)) deps job (Queue {groups, jobs, focus}) =
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    76
  let
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    77
    val id = serial ();
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    78
    val task = Task id;
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
    79
    val groups' = Inttab.cons_list (gid, task) groups;
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    80
    val jobs' = jobs
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
    81
      |> IntGraph.new_node (id, (group, Job job)) |> fold (add_job task) deps;
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    82
  in (task, make_queue groups' jobs' focus) end;
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    83
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    84
fun depend deps task (Queue {groups, jobs, focus}) =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    85
  make_queue groups (fold (add_job task) deps jobs) focus;
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    86
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    87
fun focus tasks (Queue {groups, jobs, ...}) =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    88
  make_queue groups jobs (map_filter (check_job jobs) tasks);
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    89
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    90
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    91
(* dequeue *)
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
    92
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    93
local
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    94
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    95
fun dequeue_result NONE queue = (NONE, queue)
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    96
  | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs, focus}) =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    97
      (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs) focus);
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    98
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
    99
fun dequeue_global (queue as Queue {jobs, ...}) =
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   100
  let
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   101
    fun ready (id, ((group as Group (_, ref ok), Job job), ([], _))) =
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   102
          SOME (Task id, group, (fn () => job ok))
28184
5ed5cb73a2e9 eliminated cache, access queue efficiently via IntGraph.get_first;
wenzelm
parents: 28179
diff changeset
   103
      | ready _ = NONE;
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   104
  in dequeue_result (IntGraph.get_first ready jobs) queue end;
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   105
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   106
fun dequeue_local focus (queue as Queue {jobs, ...}) =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   107
  let
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   108
    fun ready id =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   109
      (case IntGraph.get_node jobs id of
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   110
        (group as Group (_, ref ok), Job job) =>
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   111
          if null (IntGraph.imm_preds jobs id) then SOME (Task id, group, (fn () => job ok))
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   112
          else NONE
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   113
      | _ => NONE);
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   114
    val ids = map (fn Task id => id) focus;
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   115
  in dequeue_result (get_first ready (IntGraph.all_preds jobs ids)) queue end;
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   116
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   117
in
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   118
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   119
fun dequeue (queue as Queue {focus, ...}) =
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   120
  (case dequeue_local focus queue of (NONE, _) => dequeue_global queue | res => res);
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
   121
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
   122
fun dequeue_towards tasks (queue as Queue {jobs, ...}) =
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   123
  dequeue_local (map_filter (check_job jobs) tasks) queue;
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   124
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   125
end;
28185
0f20cbce4935 simplified dequeue: provide Thread.self internally;
wenzelm
parents: 28184
diff changeset
   126
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   127
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   128
(* sporadic interrupts *)
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   129
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   130
fun interrupt_thread thread = Thread.interrupt thread handle Thread _ => ();
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   131
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   132
fun interrupt (Queue {jobs, ...}) task =
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   133
  (case try (get_job jobs) task of SOME (Running thread) => interrupt_thread thread | _ => ());
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   134
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   135
fun interrupt_external queue str =
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   136
  (case Int.fromString str of SOME id => interrupt queue (Task id) | NONE => ());
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   137
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   138
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   139
(* misc operations *)
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   140
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   141
fun cancel (Queue {groups, jobs, ...}) (Group (gid, ok)) =
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
   142
  let
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   143
    val _ = ok := false;  (*invalidate any future group members*)
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
   144
    val tasks = Inttab.lookup_list groups gid;
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
   145
    val running = fold (get_job jobs #> (fn Running thread => cons thread | _ => I)) tasks [];
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   146
    val _ = List.app interrupt_thread running;
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   147
  in null running end;
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   148
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   149
fun finish (task as Task id) (Queue {groups, jobs, focus}) =
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
   150
  let
28190
0a2434cf38c9 cancel: invalidate group implicitly, via bool ref;
wenzelm
parents: 28185
diff changeset
   151
    val Group (gid, _) = get_group jobs task;
28176
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
   152
    val groups' = Inttab.remove_list (op =) (gid, task) groups;
01b21886e7f0 job: explicit 'ok' status -- false for canceled jobs;
wenzelm
parents: 28171
diff changeset
   153
    val jobs' = IntGraph.del_nodes [id] jobs;
28202
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   154
    val focus' = remove (op =) task focus;
23cb9a974630 added focus, which indicates a particular collection of high-priority tasks;
wenzelm
parents: 28196
diff changeset
   155
  in make_queue groups' jobs' focus' end;
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   156
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   157
end;