purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
authorwenzelm
Sun Aug 21 13:23:29 2011 +0200 (2011-08-21)
changeset 44341a93d25fb14fc
parent 44340 3b859b573f1a
child 44351 b7f9e764532a
purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/task_queue.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Sun Aug 21 13:10:48 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sun Aug 21 13:23:29 2011 +0200
     1.3 @@ -186,13 +186,21 @@
     1.4  (* cancellation primitives *)
     1.5  
     1.6  fun cancel_now group = (*requires SYNCHRONIZED*)
     1.7 -  Task_Queue.cancel (! queue) group;
     1.8 +  let
     1.9 +    val (tasks, threads) = Task_Queue.cancel (! queue) group;
    1.10 +    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    1.11 +  in tasks end;
    1.12 +
    1.13 +fun cancel_all () = (*requires SYNCHRONIZED*)
    1.14 +  let
    1.15 +    val (groups, threads) = Task_Queue.cancel_all (! queue);
    1.16 +    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    1.17 +  in groups end;
    1.18  
    1.19  fun cancel_later group = (*requires SYNCHRONIZED*)
    1.20   (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
    1.21    broadcast scheduler_event);
    1.22  
    1.23 -
    1.24  fun interruptible_task f x =
    1.25    (if Multithreading.available then
    1.26      Multithreading.with_attributes
    1.27 @@ -380,7 +388,7 @@
    1.28    handle exn =>
    1.29      if Exn.is_interrupt exn then
    1.30       (Multithreading.tracing 1 (fn () => "Interrupt");
    1.31 -      List.app cancel_later (Task_Queue.cancel_all (! queue));
    1.32 +      List.app cancel_later (cancel_all ());
    1.33        broadcast_work (); true)
    1.34      else reraise exn;
    1.35  
     2.1 --- a/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:10:48 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:23:29 2011 +0200
     2.3 @@ -31,8 +31,8 @@
     2.4    val known_task: queue -> task -> bool
     2.5    val all_passive: queue -> bool
     2.6    val status: queue -> {ready: int, pending: int, running: int, passive: int}
     2.7 -  val cancel: queue -> group -> task list
     2.8 -  val cancel_all: queue -> group list
     2.9 +  val cancel: queue -> group -> task list * Thread.thread list
    2.10 +  val cancel_all: queue -> group list * Thread.thread list
    2.11    val finish: task -> queue -> bool * queue
    2.12    val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
    2.13    val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
    2.14 @@ -249,15 +249,14 @@
    2.15  fun cancel (Queue {groups, jobs}) group =
    2.16    let
    2.17      val _ = cancel_group group Exn.Interrupt;
    2.18 -    val (tasks, threads) =
    2.19 +    val running =
    2.20        Tasks.fold (fn (task, _) => fn (tasks, threads) =>
    2.21            (case get_job jobs task of
    2.22              Running thread => (task :: tasks, insert Thread.equal thread threads)
    2.23            | Passive _ => (task :: tasks, threads)
    2.24            | _ => (tasks, threads)))
    2.25          (get_tasks groups (group_id group)) ([], []);
    2.26 -    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    2.27 -  in tasks end;
    2.28 +  in running end;
    2.29  
    2.30  fun cancel_all (Queue {jobs, ...}) =
    2.31    let
    2.32 @@ -270,9 +269,8 @@
    2.33            Running t => (insert eq_group group groups, insert Thread.equal t running)
    2.34          | _ => (groups, running))
    2.35        end;
    2.36 -    val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
    2.37 -    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
    2.38 -  in running_groups end;
    2.39 +    val running = Task_Graph.fold cancel_job jobs ([], []);
    2.40 +  in running end;
    2.41  
    2.42  
    2.43  (* finish *)