| author | wenzelm | 
| Wed, 26 Mar 2014 14:15:34 +0100 | |
| changeset 56293 | 9bc33476f6ac | 
| parent 52537 | 4b5941730bd8 | 
| child 62920 | a5853334c179 | 
| 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: int); fun next () = Synchronized.change_result counter (fn i => let val j = i + (1: int) in (j, j) end); in next end; end;