1.1 --- a/src/Pure/Concurrent/simple_thread.ML	Mon Oct 13 15:48:38 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Mon Oct 13 15:48:39 2008 +0200
     1.3 @@ -2,13 +2,14 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Simplified thread fork interface.
     1.8 +Simplified thread operations.
     1.9  *)
    1.10  
    1.11  signature SIMPLE_THREAD =
    1.12  sig
    1.13    val fork: bool -> (unit -> unit) -> Thread.thread
    1.14    val interrupt: Thread.thread -> unit
    1.15 +  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
    1.16  end;
    1.17  
    1.18  structure SimpleThread: SIMPLE_THREAD =
    1.19 @@ -20,4 +21,19 @@
    1.20  
    1.21  fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
    1.22  
    1.23 +
    1.24 +(* basic synchronization *)
    1.25 +
    1.26 +fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
    1.27 +  let
    1.28 +    val _ =
    1.29 +      if Mutex.trylock lock then ()
    1.30 +      else
    1.31 +       (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
    1.32 +        Mutex.lock lock;
    1.33 +        Multithreading.tracing 3 (fn () => name ^ ": ... locked"));
    1.34 +    val result = Exn.capture (restore_attributes e) ();
    1.35 +    val _ = Mutex.unlock lock;
    1.36 +  in result end) ());
    1.37 +
    1.38  end;