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