# HG changeset patch
# User wenzelm
# Date 1350501512 -7200
# Node ID 69bfd86cc711da79e8c5e98e35ab7be153eba325
# Parent  0d4106850eb225f6b2e40790c1fed8b86828313d
more robust cancel_now: avoid shooting yourself in the foot;

diff -r 0d4106850eb2 -r 69bfd86cc711 src/Pure/Concurrent/future.ML
--- 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*)
diff -r 0d4106850eb2 -r 69bfd86cc711 src/Pure/Concurrent/simple_thread.ML
--- 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;