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