src/Pure/ML-Systems/multithreading_polyml.ML
changeset 25704 df9c8074ff09
parent 24688 a5754ca5c510
child 25735 4d147263f71f
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Dec 18 22:21:41 2007 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Dec 18 22:21:42 2007 +0100
     1.3 @@ -2,17 +2,28 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Multithreading in Poly/ML 5.1 or later (cf. polyml/basis/Thread.sml).
     1.8 +Multithreading in Poly/ML 5.1 (cf. polyml/basis/Thread.sml).
     1.9  *)
    1.10  
    1.11  open Thread;
    1.12  
    1.13 +signature MULTITHREADING_POLYML =
    1.14 +sig
    1.15 +  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
    1.16 +  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
    1.17 +  structure TimeLimit: TIME_LIMIT
    1.18 +end;
    1.19 +
    1.20 +signature BASIC_MULTITHREADING =
    1.21 +sig
    1.22 +  include BASIC_MULTITHREADING
    1.23 +  include MULTITHREADING_POLYML
    1.24 +end;
    1.25 +
    1.26  signature MULTITHREADING =
    1.27  sig
    1.28    include MULTITHREADING
    1.29 -  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
    1.30 -  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
    1.31 -  structure TimeLimit: TIME_LIMIT
    1.32 +  include MULTITHREADING_POLYML
    1.33  end;
    1.34  
    1.35  structure Multithreading: MULTITHREADING =
    1.36 @@ -227,13 +238,26 @@
    1.37  
    1.38    in ! status end);
    1.39  
    1.40 +
    1.41 +(* serial numbers *)
    1.42 +
    1.43 +local
    1.44 +
    1.45 +val serial_lock = Mutex.mutex ();
    1.46 +val serial_count = ref 0;
    1.47 +
    1.48 +in
    1.49 +
    1.50 +val serial = uninterruptible (fn _ => fn () =>
    1.51 +  let
    1.52 +    val _ = Mutex.lock serial_lock;
    1.53 +    val res = inc serial_count;
    1.54 +    val _ = Mutex.unlock serial_lock;
    1.55 +  in res end);
    1.56 +
    1.57  end;
    1.58  
    1.59 -val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.60 -val CRITICAL = Multithreading.CRITICAL;
    1.61 +end;
    1.62  
    1.63 -val ignore_interrupt = Multithreading.ignore_interrupt;
    1.64 -val raise_interrupt = Multithreading.raise_interrupt;
    1.65 -
    1.66 -structure TimeLimit = Multithreading.TimeLimit;
    1.67 -
    1.68 +structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    1.69 +open BasicMultithreading;