--- a/src/Pure/Concurrent/future.ML Mon Jul 27 12:24:27 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 27 13:32:23 2009 +0200
@@ -46,7 +46,6 @@
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
val interruptible_task: ('a -> 'b) -> 'a -> 'b
- val interrupt_task: string -> unit
val cancel_group: group -> unit
val cancel: 'a future -> unit
val shutdown: unit -> unit
@@ -400,11 +399,7 @@
(fn _ => f) x
else interruptible f x;
-(*interrupt: permissive signal, may get ignored*)
-fun interrupt_task id = SYNCHRONIZED "interrupt"
- (fn () => Task_Queue.interrupt_external (! queue) id);
-
-(*cancel: present and future group members will be interrupted eventually*)
+(*cancel_group: present and future group members will be interrupted eventually*)
fun cancel_group group =
(scheduler_check "cancel check";
SYNCHRONIZED "cancel" (fn () => (do_cancel group; broadcast scheduler_event)));
--- a/src/Pure/Concurrent/task_queue.ML Mon Jul 27 12:24:27 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Mon Jul 27 13:32:23 2009 +0200
@@ -30,8 +30,6 @@
val dequeue_towards: task list -> queue ->
(((task * group * (bool -> bool) list) * task list) option * queue)
val finish: task -> queue -> bool * queue
- val interrupt: queue -> task -> unit
- val interrupt_external: queue -> string -> unit
end;
structure Task_Queue:> TASK_QUEUE =
@@ -240,20 +238,4 @@
val cache' = if maximal then cache else Unknown;
in (maximal, make_queue groups' jobs' cache') end;
-
-(* sporadic interrupts *)
-
-fun interrupt (Queue {jobs, ...}) task =
- (case try (get_job jobs) task of
- SOME (Running thread) => SimpleThread.interrupt thread
- | _ => ());
-
-fun interrupt_external (queue as Queue {jobs, ...}) str =
- (case Int.fromString str of
- SOME i =>
- (case Task_Graph.get_first NONE
- (fn (task as Task (_, j), _) => if i = j then SOME task else NONE) jobs
- of SOME task => interrupt queue task | NONE => ())
- | NONE => ());
-
end;