1(*  Title:      Pure/Concurrent/counter.ML
2    Author:     Makarius
3
4Synchronized counter for unique identifiers > 0.
5
6NB: ML ticks forwards, JVM ticks backwards.
7*)
8
9signature COUNTER =
10sig
11  val make: unit -> unit -> int
12end;
13
14structure Counter: COUNTER =
15struct
16
17fun make () =
18  let
19    val counter = Synchronized.var "counter" 0;
20    fun next () =
21      Synchronized.change_result counter
22        (fn i =>
23          let val j = i + (if Thread_Data.is_virtual then 3 else 2)
24          in (j, j) end);
25  in next end;
26
27end;
28