more official Future.terminate;
tuned signature;

--- a/src/Pure/Concurrent/future.ML	Thu Oct 18 09:19:37 2012 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 18 12:00:27 2012 +0200
@@ -63,7 +63,6 @@
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
-  val join_tasks: task list -> unit
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val cond_forks: params -> (unit -> 'a) list -> 'a future list
@@ -72,9 +71,8 @@
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
+  val terminate: group -> unit
   val shutdown: unit -> unit
-  val group_tasks: group -> task list
-  val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
 end;
 
 structure Future: FUTURE =
@@ -410,12 +408,15 @@
 
 (* cancel *)
 
-fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
+fun cancel_group_unsynchronized group = (*requires SYNCHRONIZED*)
   let
     val _ = if null (cancel_now group) then () else cancel_later group;
     val _ = signal work_available;
     val _ = scheduler_check ();
-  in () end);
+  in () end;
+
+fun cancel_group group =
+  SYNCHRONIZED "cancel_group" (fn () => cancel_group_unsynchronized group);
 
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
 
@@ -542,13 +543,6 @@
 fun joins xs = Par_Exn.release_all (join_results xs);
 fun join x = Exn.release (join_result x);
 
-fun join_tasks [] = ()
-  | join_tasks tasks =
-      (singleton o forks)
-        {name = "join_tasks", group = SOME (new_group NONE),
-          deps = tasks, pri = 0, interrupts = false} I
-      |> join;
-
 
 (* fast-path versions -- bypassing task queue *)
 
@@ -633,6 +627,24 @@
 fun fulfill x res = fulfill_result x (Exn.Res res);
 
 
+(* terminate *)
+
+fun terminate group =
+  let
+    val tasks =
+      SYNCHRONIZED "terminate" (fn () =>
+        let val _ = cancel_group_unsynchronized group;
+        in Task_Queue.group_tasks (! queue) group end);
+  in
+    if null tasks then ()
+    else
+      (singleton o forks)
+        {name = "terminate", group = SOME (new_group NONE),
+          deps = tasks, pri = 0, interrupts = false} I
+      |> join
+  end;
+
+
 (* shutdown *)
 
 fun shutdown () =
@@ -645,8 +657,6 @@
 
 (* queue status *)
 
-fun group_tasks group = Task_Queue.group_tasks (! queue) group;
-
 fun queue_status () = Task_Queue.status (! queue);
 
 

--- a/src/Pure/PIDE/document.ML	Thu Oct 18 09:19:37 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Oct 18 12:00:27 2012 +0200
@@ -318,14 +318,8 @@
 (** document execution **)
 
 val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
-
 val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
-
-fun terminate_execution state =
-  let
-    val (_, group, _) = execution_of state;
-    val _ = Future.cancel_group group;
-  in Future.join_tasks (Future.group_tasks group) end;
+val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
 
 fun start_execution state =
   let