(*  Title:      Pure/Concurrent/simple_thread.ML

    Author:     Makarius

Simplified thread operations.

*)

signature SIMPLE_THREAD =

sig

  val attributes: bool -> Thread.threadAttribute list

  val fork: bool -> (unit -> unit) -> Thread.thread

  val interrupt: Thread.thread -> unit

  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a

end;

structure SimpleThread: SIMPLE_THREAD =

struct

fun attributes interrupts =

  if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;

fun fork interrupts body =

  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),

    attributes interrupts);

fun interrupt thread = Thread.interrupt thread handle Thread _ => ();

(* basic synchronization *)

fun synchronized name lock e =

  if Multithreading.available then

    Exn.release (uninterruptible (fn restore_attributes => fn () =>

    let

      val immediate =

        if Mutex.trylock lock then true

        else

          let

            val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");

            val time = Multithreading.real_time Mutex.lock lock;

            val _ = Multithreading.tracing_time true time

              (fn () => name ^ ": locked after " ^ Time.toString time);

          in false end;

      val result = Exn.capture (restore_attributes e) ();

      val _ =

        if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");

      val _ = Mutex.unlock lock;

    in result end) ())

  else e ();

end;