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