|
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
|
|
62920
|
19 |
val counter = Synchronized.var "counter" 0;
|
|
52537
|
20 |
fun next () =
|
|
|
21 |
Synchronized.change_result counter
|
|
|
22 |
(fn i =>
|
|
62920
|
23 |
let val j = i + (if Thread_Data.is_virtual then 3 else 2)
|
|
52537
|
24 |
in (j, j) end);
|
|
|
25 |
in next end;
|
|
|
26 |
|
|
|
27 |
end;
|