more official Future.terminate;
authorwenzelm
Thu Oct 18 12:00:27 2012 +0200 (2012-10-18)
changeset 4990606a3570b0f0a
parent 49905 a81f95693c68
child 49907 c4bd02e32d35
more official Future.terminate;
tuned signature;
src/Pure/Concurrent/future.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Thu Oct 18 09:19:37 2012 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Oct 18 12:00:27 2012 +0200
     1.3 @@ -63,7 +63,6 @@
     1.4    val join_result: 'a future -> 'a Exn.result
     1.5    val joins: 'a future list -> 'a list
     1.6    val join: 'a future -> 'a
     1.7 -  val join_tasks: task list -> unit
     1.8    val value_result: 'a Exn.result -> 'a future
     1.9    val value: 'a -> 'a future
    1.10    val cond_forks: params -> (unit -> 'a) list -> 'a future list
    1.11 @@ -72,9 +71,8 @@
    1.12    val promise: (unit -> unit) -> 'a future
    1.13    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.14    val fulfill: 'a future -> 'a -> unit
    1.15 +  val terminate: group -> unit
    1.16    val shutdown: unit -> unit
    1.17 -  val group_tasks: group -> task list
    1.18 -  val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
    1.19  end;
    1.20  
    1.21  structure Future: FUTURE =
    1.22 @@ -410,12 +408,15 @@
    1.23  
    1.24  (* cancel *)
    1.25  
    1.26 -fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
    1.27 +fun cancel_group_unsynchronized group = (*requires SYNCHRONIZED*)
    1.28    let
    1.29      val _ = if null (cancel_now group) then () else cancel_later group;
    1.30      val _ = signal work_available;
    1.31      val _ = scheduler_check ();
    1.32 -  in () end);
    1.33 +  in () end;
    1.34 +
    1.35 +fun cancel_group group =
    1.36 +  SYNCHRONIZED "cancel_group" (fn () => cancel_group_unsynchronized group);
    1.37  
    1.38  fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
    1.39  
    1.40 @@ -542,13 +543,6 @@
    1.41  fun joins xs = Par_Exn.release_all (join_results xs);
    1.42  fun join x = Exn.release (join_result x);
    1.43  
    1.44 -fun join_tasks [] = ()
    1.45 -  | join_tasks tasks =
    1.46 -      (singleton o forks)
    1.47 -        {name = "join_tasks", group = SOME (new_group NONE),
    1.48 -          deps = tasks, pri = 0, interrupts = false} I
    1.49 -      |> join;
    1.50 -
    1.51  
    1.52  (* fast-path versions -- bypassing task queue *)
    1.53  
    1.54 @@ -633,6 +627,24 @@
    1.55  fun fulfill x res = fulfill_result x (Exn.Res res);
    1.56  
    1.57  
    1.58 +(* terminate *)
    1.59 +
    1.60 +fun terminate group =
    1.61 +  let
    1.62 +    val tasks =
    1.63 +      SYNCHRONIZED "terminate" (fn () =>
    1.64 +        let val _ = cancel_group_unsynchronized group;
    1.65 +        in Task_Queue.group_tasks (! queue) group end);
    1.66 +  in
    1.67 +    if null tasks then ()
    1.68 +    else
    1.69 +      (singleton o forks)
    1.70 +        {name = "terminate", group = SOME (new_group NONE),
    1.71 +          deps = tasks, pri = 0, interrupts = false} I
    1.72 +      |> join
    1.73 +  end;
    1.74 +
    1.75 +
    1.76  (* shutdown *)
    1.77  
    1.78  fun shutdown () =
    1.79 @@ -645,8 +657,6 @@
    1.80  
    1.81  (* queue status *)
    1.82  
    1.83 -fun group_tasks group = Task_Queue.group_tasks (! queue) group;
    1.84 -
    1.85  fun queue_status () = Task_Queue.status (! queue);
    1.86  
    1.87  
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Oct 18 09:19:37 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Oct 18 12:00:27 2012 +0200
     2.3 @@ -318,14 +318,8 @@
     2.4  (** document execution **)
     2.5  
     2.6  val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
     2.7 -
     2.8  val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
     2.9 -
    2.10 -fun terminate_execution state =
    2.11 -  let
    2.12 -    val (_, group, _) = execution_of state;
    2.13 -    val _ = Future.cancel_group group;
    2.14 -  in Future.join_tasks (Future.group_tasks group) end;
    2.15 +val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
    2.16  
    2.17  fun start_execution state =
    2.18    let