simplified Future.cancel/cancel_group (again) -- running threads only;
authorwenzelm
Mon Apr 09 17:22:23 2012 +0200 (2012-04-09 ago)
changeset 47404e6e5750f1311
parent 47403 296b478df14e
child 47405 559b44b5164c
simplified Future.cancel/cancel_group (again) -- running threads only;
more robust update/cancel_execution: full join_tasks of group before exec state assignment;
tuned signature;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Apr 09 15:10:52 2012 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Apr 09 17:22:23 2012 +0200
     1.3 @@ -52,8 +52,8 @@
     1.4    val peek: 'a future -> 'a Exn.result option
     1.5    val is_finished: 'a future -> bool
     1.6    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.7 -  val cancel_group: group -> task list
     1.8 -  val cancel: 'a future -> task list
     1.9 +  val cancel_group: group -> unit
    1.10 +  val cancel: 'a future -> unit
    1.11    type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
    1.12    val default_params: params
    1.13    val forks: params -> (unit -> 'a) list -> 'a future list
    1.14 @@ -74,6 +74,8 @@
    1.15    val fulfill: 'a future -> 'a -> unit
    1.16    val shutdown: unit -> unit
    1.17    val status: (unit -> 'a) -> 'a
    1.18 +  val group_tasks: group -> task list
    1.19 +  val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
    1.20  end;
    1.21  
    1.22  structure Future: FUTURE =
    1.23 @@ -181,9 +183,9 @@
    1.24  
    1.25  fun cancel_now group = (*requires SYNCHRONIZED*)
    1.26    let
    1.27 -    val (tasks, threads) = Task_Queue.cancel (! queue) group;
    1.28 -    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    1.29 -  in tasks end;
    1.30 +    val running = Task_Queue.cancel (! queue) group;
    1.31 +    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
    1.32 +  in running end;
    1.33  
    1.34  fun cancel_all () = (*requires SYNCHRONIZED*)
    1.35    let
    1.36 @@ -413,7 +415,7 @@
    1.37      val _ =
    1.38        if null running then ()
    1.39        else (cancel_later group; signal work_available; scheduler_check ());
    1.40 -  in running end);
    1.41 +  in () end);
    1.42  
    1.43  fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
    1.44  
    1.45 @@ -650,6 +652,13 @@
    1.46    in x end;
    1.47  
    1.48  
    1.49 +(* queue status *)
    1.50 +
    1.51 +fun group_tasks group = Task_Queue.group_tasks (! queue) group;
    1.52 +
    1.53 +fun queue_status () = Task_Queue.status (! queue);
    1.54 +
    1.55 +
    1.56  (*final declarations of this structure!*)
    1.57  val map = map_future;
    1.58  
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Mon Apr 09 15:10:52 2012 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Mon Apr 09 17:22:23 2012 +0200
     2.3 @@ -39,8 +39,7 @@
     2.4          Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
     2.5            (map (fn x => fn () => f x) xs);
     2.6        val results = Future.join_results futures
     2.7 -        handle exn =>
     2.8 -          (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
     2.9 +        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
    2.10      in results end;
    2.11  
    2.12  fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
     3.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon Apr 09 15:10:52 2012 +0200
     3.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon Apr 09 17:22:23 2012 +0200
     3.3 @@ -28,10 +28,11 @@
     3.4    val waiting: task -> task list -> (unit -> 'a) -> 'a
     3.5    type queue
     3.6    val empty: queue
     3.7 +  val group_tasks: queue -> group -> task list
     3.8    val known_task: queue -> task -> bool
     3.9    val all_passive: queue -> bool
    3.10    val status: queue -> {ready: int, pending: int, running: int, passive: int}
    3.11 -  val cancel: queue -> group -> task list * Thread.thread list
    3.12 +  val cancel: queue -> group -> Thread.thread list
    3.13    val cancel_all: queue -> group list * Thread.thread list
    3.14    val finish: task -> queue -> bool * queue
    3.15    val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
    3.16 @@ -210,6 +211,7 @@
    3.17  fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
    3.18  val empty = make_queue Inttab.empty Task_Graph.empty;
    3.19  
    3.20 +fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
    3.21  fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
    3.22  
    3.23  
    3.24 @@ -254,12 +256,9 @@
    3.25    let
    3.26      val _ = cancel_group group Exn.Interrupt;
    3.27      val running =
    3.28 -      Tasks.fold (fn (task, _) => fn (tasks, threads) =>
    3.29 -          (case get_job jobs task of
    3.30 -            Running thread => (task :: tasks, insert Thread.equal thread threads)
    3.31 -          | Passive _ => (task :: tasks, threads)
    3.32 -          | _ => (tasks, threads)))
    3.33 -        (get_tasks groups (group_id group)) ([], []);
    3.34 +      Tasks.fold (fn (task, _) =>
    3.35 +          (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
    3.36 +        (get_tasks groups (group_id group)) [];
    3.37    in running end;
    3.38  
    3.39  fun cancel_all (Queue {jobs, ...}) =
     4.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 09 15:10:52 2012 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 09 17:22:23 2012 +0200
     4.3 @@ -26,7 +26,7 @@
     4.4    val init_state: state
     4.5    val define_command: command_id -> string -> string -> state -> state
     4.6    val discontinue_execution: state -> unit
     4.7 -  val cancel_execution: state -> Future.task list
     4.8 +  val cancel_execution: state -> unit
     4.9    val execute: version_id -> state -> state
    4.10    val update: version_id -> version_id -> edit list -> state ->
    4.11      (command_id * exec_id option) list * state
    4.12 @@ -301,6 +301,7 @@
    4.13  fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false;
    4.14  
    4.15  fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group;
    4.16 +fun execution_tasks (State {execution = (_, group, _), ...}) = Future.group_tasks group;
    4.17  
    4.18  end;
    4.19  
    4.20 @@ -476,6 +477,7 @@
    4.21      val nodes = nodes_of new_version;
    4.22      val is_required = make_required nodes;
    4.23  
    4.24 +    val _ = Future.join_tasks (execution_tasks state);
    4.25      val updated =
    4.26        nodes |> Graph.schedule
    4.27          (fn deps => fn (name, node) =>
     5.1 --- a/src/Pure/PIDE/protocol.ML	Mon Apr 09 15:10:52 2012 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Apr 09 17:22:23 2012 +0200
     5.3 @@ -18,12 +18,14 @@
     5.4  
     5.5  val _ =
     5.6    Isabelle_Process.protocol_command "Document.cancel_execution"
     5.7 -    (fn [] => ignore (Document.cancel_execution (Document.state ())));
     5.8 +    (fn [] => Document.cancel_execution (Document.state ()));
     5.9  
    5.10  val _ =
    5.11    Isabelle_Process.protocol_command "Document.update"
    5.12      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    5.13        let
    5.14 +        val _ = Document.cancel_execution state;
    5.15 +
    5.16          val old_id = Document.parse_id old_id_string;
    5.17          val new_id = Document.parse_id new_id_string;
    5.18          val edits =
    5.19 @@ -48,9 +50,7 @@
    5.20                    fn (a, []) => Document.Perspective (map int_atom a)]))
    5.21              end;
    5.22  
    5.23 -        val running = Document.cancel_execution state;
    5.24          val (assignment, state1) = Document.update old_id new_id edits state;
    5.25 -        val _ = Future.join_tasks running;
    5.26          val _ =
    5.27            Output.protocol_message Isabelle_Markup.assign_execs
    5.28              ((new_id, assignment) |>