# HG changeset patch
# User wenzelm
# Date 1223578397 -7200
# Node ID 422e9bd169acf99f6af6ec67585f1bea3e25e103
# Parent  78affc7d4d0f3c4ca8554332952ecf7637c1cd6c
added fail-safe interrupt;

diff -r 78affc7d4d0f -r 422e9bd169ac src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Thu Oct 09 20:53:16 2008 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Thu Oct 09 20:53:17 2008 +0200
@@ -8,6 +8,7 @@
 signature SIMPLE_THREAD =
 sig
   val fork: bool -> (unit -> unit) -> Thread.thread
+  val interrupt: Thread.thread -> unit
 end;
 
 structure SimpleThread: SIMPLE_THREAD =
@@ -17,4 +18,6 @@
   Thread.fork (fn () => exception_trace (fn () => body ()),
     if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
 
+fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
+
 end;