src/Pure/Concurrent/simple_thread.ML

proof_body/pthm: removed redundant types field;
fold_proof_atoms: unified recursive case with fold_body_thms;
tuned signature;

(*  Title:      Pure/Concurrent/simple_thread.ML
    ID:         $Id$
    Author:     Makarius

Simplified thread operations.
*)

signature SIMPLE_THREAD =
sig
  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 fork interrupts body =
  Thread.fork (fn () => exception_trace (fn () => body ()),
    if interrupts then Multithreading.regular_interrupts else Multithreading.no_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 _ =
      if Mutex.trylock lock then ()
      else
       (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
        Mutex.lock lock;
        Multithreading.tracing 3 (fn () => name ^ ": ... locked"));
    val result = Exn.capture (restore_attributes e) ();
    val _ = Mutex.unlock lock;
  in result end) ());

end;