# HG changeset patch
# User wenzelm
# Date 1198012902 -3600
# Node ID df9c8074ff09bcfb989c3f529cdb8914337b85b9
# Parent  832073e402ae9d8934fe1c5d33da6b2575aa348d
signature BASIC_MULTITHREADING;
added specific serial number generator, which avoid the global CRITICAL lock;

diff -r 832073e402ae -r df9c8074ff09 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Tue Dec 18 22:21:41 2007 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Tue Dec 18 22:21:42 2007 +0100
@@ -5,18 +5,24 @@
 Dummy implementation of multithreading interface.
 *)
 
+signature BASIC_MULTITHREADING =
+sig
+  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
+  val CRITICAL: (unit -> 'a) -> 'a
+end;
+
 signature MULTITHREADING =
 sig
+  include BASIC_MULTITHREADING
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val available: bool
   val max_threads: int ref
   val self_critical: unit -> bool
-  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
-  val CRITICAL: (unit -> 'a) -> 'a
   datatype 'a task =
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
   val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
+  val serial: unit -> int
 end;
 
 structure Multithreading: MULTITHREADING =
@@ -37,7 +43,11 @@
 
 fun schedule _ _ _ = raise Fail "No multithreading support";
 
+local val count = ref (0: int)
+in fun serial () = (count := ! count + 1; ! count) end;
+
 end;
 
-val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
-val CRITICAL = Multithreading.CRITICAL;
+structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
+open BasicMultithreading;
+
diff -r 832073e402ae -r df9c8074ff09 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Dec 18 22:21:41 2007 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Dec 18 22:21:42 2007 +0100
@@ -2,17 +2,28 @@
     ID:         $Id$
     Author:     Makarius
 
-Multithreading in Poly/ML 5.1 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML 5.1 (cf. polyml/basis/Thread.sml).
 *)
 
 open Thread;
 
+signature MULTITHREADING_POLYML =
+sig
+  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
+  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
+  structure TimeLimit: TIME_LIMIT
+end;
+
+signature BASIC_MULTITHREADING =
+sig
+  include BASIC_MULTITHREADING
+  include MULTITHREADING_POLYML
+end;
+
 signature MULTITHREADING =
 sig
   include MULTITHREADING
-  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
-  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
-  structure TimeLimit: TIME_LIMIT
+  include MULTITHREADING_POLYML
 end;
 
 structure Multithreading: MULTITHREADING =
@@ -227,13 +238,26 @@
 
   in ! status end);
 
+
+(* serial numbers *)
+
+local
+
+val serial_lock = Mutex.mutex ();
+val serial_count = ref 0;
+
+in
+
+val serial = uninterruptible (fn _ => fn () =>
+  let
+    val _ = Mutex.lock serial_lock;
+    val res = inc serial_count;
+    val _ = Mutex.unlock serial_lock;
+  in res end);
+
 end;
 
-val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
-val CRITICAL = Multithreading.CRITICAL;
+end;
 
-val ignore_interrupt = Multithreading.ignore_interrupt;
-val raise_interrupt = Multithreading.raise_interrupt;
-
-structure TimeLimit = Multithreading.TimeLimit;
-
+structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
+open BasicMultithreading;