1.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Jul 23 20:34:33 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Jul 23 21:29:56 2011 +0200
     1.3 @@ -14,12 +14,14 @@
     1.4    val is_canceled: group -> bool
     1.5    val group_status: group -> exn list
     1.6    val str_of_group: group -> string
     1.7 +  val str_of_groups: group -> string
     1.8    type task
     1.9    val dummy_task: unit -> task
    1.10    val group_of_task: task -> group
    1.11    val name_of_task: task -> string
    1.12    val pri_of_task: task -> int
    1.13    val str_of_task: task -> string
    1.14 +  val str_of_task_groups: task -> string
    1.15    val timing_of_task: task -> Time.time * Time.time * string list
    1.16    val running: task -> (unit -> 'a) -> 'a
    1.17    val joining: task -> (unit -> 'a) -> 'a
    1.18 @@ -64,8 +66,8 @@
    1.19  fun group_id (Group {id, ...}) = id;
    1.20  fun eq_group (group1, group2) = group_id group1 = group_id group2;
    1.21  
    1.22 -fun group_ancestry f (Group {parent = NONE, id, ...}) a = f id a
    1.23 -  | group_ancestry f (Group {parent = SOME group, id, ...}) a = group_ancestry f group (f id a);
    1.24 +fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a
    1.25 +  | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a);
    1.26  
    1.27  
    1.28  (* group status *)
    1.29 @@ -87,6 +89,9 @@
    1.30  fun str_of_group group =
    1.31    (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
    1.32  
    1.33 +fun str_of_groups group =
    1.34 +  space_implode "/" (map str_of_group (rev (fold_groups cons group [])));
    1.35 +
    1.36  end;
    1.37  
    1.38  
    1.39 @@ -114,9 +119,12 @@
    1.40  fun group_of_task (Task {group, ...}) = group;
    1.41  fun name_of_task (Task {name, ...}) = name;
    1.42  fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
    1.43 +
    1.44  fun str_of_task (Task {name, id, ...}) =
    1.45    if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
    1.46  
    1.47 +fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
    1.48 +
    1.49  fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
    1.50  
    1.51  fun update_timing update (Task {timing, ...}) e =
    1.52 @@ -263,7 +271,7 @@
    1.53  fun finish task (Queue {groups, jobs}) =
    1.54    let
    1.55      val group = group_of_task task;
    1.56 -    val groups' = group_ancestry (fn gid => del_task (gid, task)) group groups;
    1.57 +    val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
    1.58      val jobs' = Task_Graph.del_node task jobs;
    1.59      val maximal = null (Task_Graph.imm_succs jobs task);
    1.60    in (maximal, make_queue groups' jobs') end;
    1.61 @@ -274,14 +282,14 @@
    1.62  fun enqueue_passive group abort (Queue {groups, jobs}) =
    1.63    let
    1.64      val task = new_task group "passive" NONE;
    1.65 -    val groups' = group_ancestry (fn gid => add_task (gid, task)) group groups;
    1.66 +    val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
    1.67      val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
    1.68    in (task, make_queue groups' jobs') end;
    1.69  
    1.70  fun enqueue name group deps pri job (Queue {groups, jobs}) =
    1.71    let
    1.72      val task = new_task group name (SOME pri);
    1.73 -    val groups' = group_ancestry (fn gid => add_task (gid, task)) group groups;
    1.74 +    val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
    1.75      val jobs' = jobs
    1.76        |> Task_Graph.new_node (task, Job [job])
    1.77        |> fold (add_job task) deps;