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