diff -r c07ae96cbfc4 -r 9e7e1e309ebd src/Pure/ML-Systems/multithreading_polyml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 24 19:44:32 2007 +0200
@@ -0,0 +1,55 @@
+(*  Title:      Pure/ML-Systems/multithreading_polyml.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Multithreading in Poly/ML (version 5.1).
+*)
+
+open Thread;
+
+structure Multithreading: MULTITHREADING =
+struct
+
+val number_of_threads = ref 0;
+
+
+(* FIXME tmp *)
+fun message s =
+  (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
+
+
+(* critical section -- may be nested within the same thread *)
+
+local
+
+val critical_lock = Mutex.mutex ();
+val critical_thread = ref (NONE: Thread.thread option);
+
+in
+
+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 result = Exn.capture e ();
+      val _ = critical_thread := NONE;
+      val _ = Mutex.unlock critical_lock;
+    in Exn.release result end;
+
+end;
+
+end;
+
+val CRITICAL = Multithreading.CRITICAL;