# HG changeset patch
# User wenzelm
# Date 1248694343 -7200
# Node ID 572b923624963c478cfb2c464154440964598a32
# Parent  fcbd6c9ee9bb1d1bc9fc137c68c3e7dfb016d881
removed unused low-level interrupts;

diff -r fcbd6c9ee9bb -r 572b92362496 src/Pure/Concurrent/future.ML
--- 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)));
diff -r fcbd6c9ee9bb -r 572b92362496 src/Pure/Concurrent/task_queue.ML
--- 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;