author | wenzelm |
Sun, 12 Mar 2017 18:50:02 +0100 | |
changeset 65202 | 187277b77d50 |
parent 62920 | a5853334c179 |
child 68804 | cbde6e3b132b |
permissions | -rw-r--r-- |
(* Title: Pure/Concurrent/counter.ML Author: Makarius Synchronized counter for unique identifiers > 0. NB: ML ticks forwards, JVM ticks backwards. *) signature COUNTER = sig val make: unit -> unit -> int end; structure Counter: COUNTER = struct fun make () = let val counter = Synchronized.var "counter" 0; fun next () = Synchronized.change_result counter (fn i => let val j = i + (if Thread_Data.is_virtual then 3 else 2) in (j, j) end); in next end; end;