1.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 13:32:29 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 15:06:33 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    val extend: task -> (bool -> bool) -> queue -> queue option
     1.5    val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
     1.6    val dequeue_towards: task list -> queue ->
     1.7 -    (((task * group * (bool -> bool) list) * task list) option * queue)
     1.8 +    (((task * group * (bool -> bool) list) option * task list) * queue)
     1.9    val finish: task -> queue -> bool * queue
    1.10  end;
    1.11  
    1.12 @@ -215,14 +215,14 @@
    1.13        let
    1.14          val jobs' = set_job task (Running (Thread.self ())) jobs;
    1.15          val cache' = Unknown;
    1.16 -      in (SOME (res, tasks), make_queue groups jobs' cache') end;
    1.17 +      in ((SOME res, tasks), make_queue groups jobs' cache') end;
    1.18    in
    1.19      (case get_first ready tasks of
    1.20        SOME res => result res
    1.21      | NONE =>
    1.22          (case get_first (get_first ready o Task_Graph.imm_preds jobs) tasks of
    1.23            SOME res => result res
    1.24 -        | NONE => (NONE, queue)))
    1.25 +        | NONE => ((NONE, tasks), queue)))
    1.26    end;
    1.27  
    1.28