--- a/src/Pure/Concurrent/future.ML Wed Oct 17 21:04:51 2012 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Oct 17 21:18:32 2012 +0200
@@ -183,7 +183,9 @@
fun cancel_now group = (*requires SYNCHRONIZED*)
let
val running = Task_Queue.cancel (! queue) group;
- val _ = List.app Simple_Thread.interrupt_unsynchronized running;
+ val _ = running |> List.app (fn thread =>
+ if Simple_Thread.is_self thread then ()
+ else Simple_Thread.interrupt_unsynchronized thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)
--- a/src/Pure/Concurrent/simple_thread.ML Wed Oct 17 21:04:51 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Oct 17 21:18:32 2012 +0200
@@ -6,6 +6,7 @@
signature SIMPLE_THREAD =
sig
+ val is_self: Thread.thread -> bool
val attributes: bool -> Thread.threadAttribute list
val fork: bool -> (unit -> unit) -> Thread.thread
val interrupt_unsynchronized: Thread.thread -> unit
@@ -15,6 +16,8 @@
structure Simple_Thread: SIMPLE_THREAD =
struct
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
fun attributes interrupts =
if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;