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