--- 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;