# HG changeset patch
# User wenzelm
# Date 1257891315 -3600
# Node ID d25e6bd6ca95f35f1b348318dbf0225bbab452f8
# Parent  4608243edcfce3098bc89bfb8fce980e348d1e40
exported SimpleThread.attributes;

diff -r 4608243edcfc -r d25e6bd6ca95 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Tue Nov 10 21:28:46 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Nov 10 23:15:15 2009 +0100
@@ -6,6 +6,7 @@
 
 signature SIMPLE_THREAD =
 sig
+  val attributes: bool -> Thread.threadAttribute list
   val fork: bool -> (unit -> unit) -> Thread.thread
   val interrupt: Thread.thread -> unit
   val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
@@ -14,9 +15,12 @@
 structure SimpleThread: SIMPLE_THREAD =
 struct
 
+fun attributes interrupts =
+  if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
+
 fun fork interrupts body =
   Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
-    if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
+    attributes interrupts);
 
 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();