1.1 --- a/src/Pure/Concurrent/task_queue.ML	Sun Jun 14 23:24:38 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sun Jun 14 23:25:49 2009 +0200
     1.3 @@ -21,7 +21,6 @@
     1.4    val is_empty: queue -> bool
     1.5    val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
     1.6    val extend: task -> (bool -> bool) -> queue -> queue option
     1.7 -  val depend: task list -> task -> queue -> queue
     1.8    val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
     1.9    val interrupt: queue -> task -> unit
    1.10    val interrupt_external: queue -> string -> unit
    1.11 @@ -74,9 +73,6 @@
    1.12  fun add_job task dep (jobs: jobs) =
    1.13    Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
    1.14  
    1.15 -fun add_job_acyclic task dep (jobs: jobs) =
    1.16 -  Task_Graph.add_edge_acyclic (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
    1.17 -
    1.18  
    1.19  (* queue of grouped jobs *)
    1.20  
    1.21 @@ -95,22 +91,25 @@
    1.22  
    1.23  (* enqueue *)
    1.24  
    1.25 -fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, ...}) =
    1.26 +fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) =
    1.27    let
    1.28      val task = new_task pri;
    1.29      val groups' = Inttab.cons_list (gid, task) groups;
    1.30      val jobs' = jobs
    1.31        |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
    1.32 -  in (task, make_queue groups' jobs' Unknown) end;
    1.33 +    val cache' =
    1.34 +      (case cache of
    1.35 +        Result last =>
    1.36 +          if task_ord (last, task) = LESS
    1.37 +          then cache else Unknown
    1.38 +      | _ => Unknown);
    1.39 +  in (task, make_queue groups' jobs' cache') end;
    1.40  
    1.41  fun extend task job (Queue {groups, jobs, cache}) =
    1.42    (case try (get_job jobs) task of
    1.43      SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) cache)
    1.44    | _ => NONE);
    1.45  
    1.46 -fun depend deps task (Queue {groups, jobs, ...}) =
    1.47 -  make_queue groups (fold (add_job_acyclic task) deps jobs) Unknown;
    1.48 -
    1.49  
    1.50  (* dequeue *)
    1.51  
    1.52 @@ -168,11 +167,14 @@
    1.53      val _ = List.app SimpleThread.interrupt running;
    1.54    in groups end;
    1.55  
    1.56 -fun finish task (Queue {groups, jobs, ...}) =
    1.57 +fun finish task (Queue {groups, jobs, cache}) =
    1.58    let
    1.59      val Group (gid, _) = get_group jobs task;
    1.60      val groups' = Inttab.remove_list (op =) (gid, task) groups;
    1.61      val jobs' = Task_Graph.del_node task jobs;
    1.62 -  in make_queue groups' jobs' Unknown end;
    1.63 +    val cache' =
    1.64 +      if null (Task_Graph.imm_succs jobs task) then cache
    1.65 +      else Unknown;
    1.66 +  in make_queue groups' jobs' cache' end;
    1.67  
    1.68  end;