# HG changeset patch
# User wenzelm
# Date 1223905719 -7200
# Node ID bd2456e0d944e958b674406ab72422be34e2e144
# Parent  dc4aae271c411630418d82f99364ed3e272c94d3
added generic combinator for synchronized evaluation (formerly in future.ML);

diff -r dc4aae271c41 -r bd2456e0d944 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Mon Oct 13 15:48:38 2008 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Mon Oct 13 15:48:39 2008 +0200
@@ -2,13 +2,14 @@
     ID:         $Id$
     Author:     Makarius
 
-Simplified thread fork interface.
+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 =
@@ -20,4 +21,19 @@
 
 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;