author | wenzelm |
Sun, 01 Mar 2009 23:36:12 +0100 | |
changeset 30190 | 479806475f3c |
parent 29564 | f8b933a62151 |
child 32051 | 82a9875b8707 |
permissions | -rw-r--r-- |
28241 | 1 |
(* Title: Pure/Concurrent/simple_thread.ML |
2 |
Author: Makarius |
|
3 |
||
28577
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
4 |
Simplified thread operations. |
28241 | 5 |
*) |
6 |
||
7 |
signature SIMPLE_THREAD = |
|
8 |
sig |
|
9 |
val fork: bool -> (unit -> unit) -> Thread.thread |
|
28550 | 10 |
val interrupt: Thread.thread -> unit |
28577
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
11 |
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a |
28241 | 12 |
end; |
13 |
||
14 |
structure SimpleThread: SIMPLE_THREAD = |
|
15 |
struct |
|
16 |
||
17 |
fun fork interrupts body = |
|
18 |
Thread.fork (fn () => exception_trace (fn () => body ()), |
|
19 |
if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts); |
|
20 |
||
28550 | 21 |
fun interrupt thread = Thread.interrupt thread handle Thread _ => (); |
22 |
||
28577
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
23 |
|
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
24 |
(* basic synchronization *) |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
25 |
|
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
26 |
fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () => |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
27 |
let |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
28 |
val _ = |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
29 |
if Mutex.trylock lock then () |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
30 |
else |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
31 |
(Multithreading.tracing 3 (fn () => name ^ ": locking ..."); |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
32 |
Mutex.lock lock; |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
33 |
Multithreading.tracing 3 (fn () => name ^ ": ... locked")); |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
34 |
val result = Exn.capture (restore_attributes e) (); |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
35 |
val _ = Mutex.unlock lock; |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
36 |
in result end) ()); |
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
37 |
|
28241 | 38 |
end; |