1 (* Title: Pure/Concurrent/simple_thread.ML
4 Simplified thread operations.
7 signature SIMPLE_THREAD =
9 val fork: bool -> (unit -> unit) -> Thread.thread
10 val interrupt: Thread.thread -> unit
11 val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
14 structure SimpleThread: SIMPLE_THREAD =
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 _ => ();
24 (* basic synchronization *)
26 fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
29 if Mutex.trylock lock then true
32 val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
33 val time = Multithreading.real_time Mutex.lock lock;
34 val _ = Multithreading.tracing_time time
35 (fn () => name ^ ": locked after " ^ Time.toString time);
37 val result = Exn.capture (restore_attributes e) ();
39 if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
40 val _ = Mutex.unlock lock;