src/Pure/Concurrent/task_queue.ML
changeset 66166 c88d1c36c9c3
parent 63806 c54a53ef1873
child 66378 53a6c5d4d03e
equal deleted inserted replaced
66161:c6e9c7d140ff 66166:c88d1c36c9c3
    35   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
    35   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
    36   val cancel: queue -> group -> Thread.thread list
    36   val cancel: queue -> group -> Thread.thread list
    37   val cancel_all: queue -> group list * Thread.thread list
    37   val cancel_all: queue -> group list * Thread.thread list
    38   val finish: task -> queue -> bool * queue
    38   val finish: task -> queue -> bool * queue
    39   val enroll: Thread.thread -> string -> group -> queue -> task * queue
    39   val enroll: Thread.thread -> string -> group -> queue -> task * queue
    40   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
    40   val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
    41   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
    41   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
    42   val extend: task -> (bool -> bool) -> queue -> queue option
    42   val extend: task -> (bool -> bool) -> queue -> queue option
    43   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
    43   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
    44   val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
    44   val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
    45   val dequeue_deps: Thread.thread -> task list -> queue ->
    45   val dequeue_deps: Thread.thread -> task list -> queue ->
   310   in (task, make_queue groups' jobs' urgent) end;
   310   in (task, make_queue groups' jobs' urgent) end;
   311 
   311 
   312 
   312 
   313 (* enqueue *)
   313 (* enqueue *)
   314 
   314 
   315 fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
   315 fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) =
   316   let
   316   let
   317     val task = new_task group "passive" NONE;
   317     val task = new_task group name NONE;
   318     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   318     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   319     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
   319     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
   320   in (task, make_queue groups' jobs' urgent) end;
   320   in (task, make_queue groups' jobs' urgent) end;
   321 
   321 
   322 fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =
   322 fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =