# HG changeset patch
# User wenzelm
# Date 1185221885 -7200
# Node ID 5e396bcf749e5937c19c5ef3b0415c7c9b3a47e4
# Parent  4fbb1ff123376a2bbd972a5be13d48eabcc60333
added proper implementation of self_critical, CRITICAL;

diff -r 4fbb1ff12337 -r 5e396bcf749e src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Mon Jul 23 22:18:03 2007 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Mon Jul 23 22:18:05 2007 +0200
@@ -39,3 +39,54 @@
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
   in use_text name output verbose txt end;
+
+
+
+(** multithreading **)
+
+open Thread;
+
+local
+
+datatype 'a result =
+  Result of 'a |
+  Exn of exn;
+
+fun capture f x = Result (f x) handle e => Exn e;
+
+fun release (Result y) = y
+  | release (Exn e) = raise e;
+
+fun message s =
+  (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
+
+
+val critical_lock = Mutex.mutex ();
+val critical_thread = ref (NONE: Thread.thread option);
+
+in
+
+(* critical section -- may be nested within the same thread *)
+
+fun self_critical () =
+  (case ! critical_thread of
+    NONE => false
+  | SOME id => Thread.equal (id, Thread.self ()));
+
+fun CRITICAL e =
+  if self_critical () then e ()
+  else
+    let
+      val _ =
+        if Mutex.trylock critical_lock then ()
+        else
+          (message "Waiting for critical lock";
+           Mutex.lock critical_lock;
+           message "Obtained critical lock");
+      val _ = critical_thread := SOME (Thread.self ());
+      val res = capture e ();
+      val _ = critical_thread := NONE;
+      val _ = Mutex.unlock critical_lock;
+    in release res end;
+
+end;