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 timer = Timer.startRealTimer ();
33 val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
34 val _ = Mutex.lock lock;
35 val time = Timer.checkRealTimer timer;
36 val _ = Multithreading.tracing_time time (fn () =>
37 name ^ ": locked after " ^ Time.toString time);
39 val result = Exn.capture (restore_attributes e) ();
41 if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
42 val _ = Mutex.unlock lock;