| author | wenzelm |
| Thu, 09 Oct 2008 20:53:17 +0200 | |
| changeset 28550 | 422e9bd169ac |
| parent 28241 | de20fccf6509 |
| child 28577 | bd2456e0d944 |
| permissions | -rw-r--r-- |
1 (* Title: Pure/Concurrent/simple_thread.ML
2 ID: $Id$
3 Author: Makarius
5 Simplified thread fork interface.
6 *)
8 signature SIMPLE_THREAD =
9 sig
10 val fork: bool -> (unit -> unit) -> Thread.thread
11 val interrupt: Thread.thread -> unit
12 end;
14 structure SimpleThread: SIMPLE_THREAD =
15 struct
17 fun fork interrupts body =
18 Thread.fork (fn () => exception_trace (fn () => body ()),
19 if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
21 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
23 end;