(*  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 = 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) ());

end;