# HG changeset patch
# User wenzelm
# Date 1422536282 -3600
# Node ID 58c4f3e1870fb5717e41bdef3d06122d0963edbb
# Parent  6fab87db556c7723d1365e062afad7f9d3d1af56
unused;

diff -r 6fab87db556c -r 58c4f3e1870f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jan 29 13:50:53 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Jan 29 13:58:02 2015 +0100
@@ -42,7 +42,6 @@
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
   val group_snapshot: group -> task list
-  val terminate: group -> unit
   val shutdown: unit -> unit
 end;
 
@@ -640,15 +639,6 @@
     Task_Queue.group_tasks (! queue) group);
 
 
-(* terminate *)
-
-fun terminate group =
-  SYNCHRONIZED "terminate" (fn () =>
-    let val _ = cancel_group_unsynchronized group;
-    in Task_Queue.group_tasks (! queue) group end)
-  |> join_tasks;
-
-
 (* shutdown *)
 
 fun shutdown () =
diff -r 6fab87db556c -r 58c4f3e1870f src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Thu Jan 29 13:50:53 2015 +0100
+++ b/src/Pure/PIDE/execution.ML	Thu Jan 29 13:58:02 2015 +0100
@@ -14,7 +14,6 @@
   val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
   val peek: Document_ID.exec -> Future.group list
   val cancel: Document_ID.exec -> unit
-  val terminate: Document_ID.exec -> unit
   type params = {name: string, pos: Position.T, pri: int}
   val fork: params -> (unit -> 'a) -> 'a future
   val print: params -> (unit -> unit) -> unit
@@ -76,7 +75,6 @@
   | NONE => []);
 
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
-fun terminate exec_id = List.app Future.terminate (peek exec_id);
 
 
 (* fork *)