1.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 21:54:49 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon Jan 31 22:57:01 2011 +0100
     1.3 @@ -28,7 +28,8 @@
     1.4    val cancel: queue -> group -> bool
     1.5    val cancel_all: queue -> group list
     1.6    val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
     1.7 -  val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
     1.8 +  val enqueue: string -> group -> task list -> int -> (bool -> bool) ->
     1.9 +    queue -> (task * bool) * queue
    1.10    val extend: task -> (bool -> bool) -> queue -> queue option
    1.11    val dequeue_passive: Thread.thread -> task -> queue -> bool * queue
    1.12    val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
    1.13 @@ -62,21 +63,26 @@
    1.14  
    1.15  (* tasks *)
    1.16  
    1.17 -abstype task = Task of (int option * int) * timing Synchronized.var
    1.18 +abstype task = Task of
    1.19 + {name: string,
    1.20 +  id: int,
    1.21 +  pri: int option,
    1.22 +  timing: timing Synchronized.var}
    1.23  with
    1.24  
    1.25 -val dummy_task = Task ((NONE, ~1), new_timing ());
    1.26 -fun new_task pri = Task ((pri, new_id ()), new_timing ());
    1.27 +val dummy_task = Task {name = "", id = ~1, pri = NONE, timing = new_timing ()};
    1.28 +fun new_task name pri = Task {name = name, id = new_id (), pri = pri, timing = new_timing ()};
    1.29  
    1.30 -fun pri_of_task (Task ((pri, _), _)) = the_default 0 pri;
    1.31 -fun str_of_task (Task ((_, i), _)) = string_of_int i;
    1.32 +fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
    1.33 +fun str_of_task (Task {name, id, ...}) =
    1.34 +  if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
    1.35  
    1.36 -fun timing_of_task (Task (_, timing)) = Synchronized.value timing;
    1.37 -fun running (Task (_, timing)) = gen_timing apfst timing;
    1.38 -fun waiting (Task (_, timing)) = gen_timing apsnd timing;
    1.39 +fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
    1.40 +fun running (Task {timing, ...}) = gen_timing apfst timing;
    1.41 +fun waiting (Task {timing, ...}) = gen_timing apsnd timing;
    1.42  
    1.43 -fun task_ord (Task (t1, _), Task (t2, _)) =
    1.44 -  prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2);
    1.45 +fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
    1.46 +  prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
    1.47  
    1.48  val eq_task = is_equal o task_ord;
    1.49  
    1.50 @@ -219,15 +225,15 @@
    1.51  
    1.52  fun enqueue_passive group abort (Queue {groups, jobs}) =
    1.53    let
    1.54 -    val task = new_task NONE;
    1.55 +    val task = new_task "" NONE;
    1.56      val groups' = groups
    1.57        |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
    1.58      val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive abort));
    1.59    in (task, make_queue groups' jobs') end;
    1.60  
    1.61 -fun enqueue group deps pri job (Queue {groups, jobs}) =
    1.62 +fun enqueue name group deps pri job (Queue {groups, jobs}) =
    1.63    let
    1.64 -    val task = new_task (SOME pri);
    1.65 +    val task = new_task name (SOME pri);
    1.66      val groups' = groups
    1.67        |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
    1.68      val jobs' = jobs