--- a/src/Pure/Concurrent/synchronized.ML Tue Nov 09 21:13:06 2010 +0100
+++ b/src/Pure/Concurrent/synchronized.ML Tue Nov 09 21:44:19 2010 +0100
@@ -13,6 +13,7 @@
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
val change: 'a var -> ('a -> 'a) -> unit
+ val counter: unit -> unit -> int
end;
structure Synchronized: SYNCHRONIZED =
@@ -65,4 +66,17 @@
end;
+
+(* unique identifiers > 0 *)
+
+fun counter () =
+ let
+ val counter = var "counter" 0;
+ fun next () =
+ change_result counter
+ (fn i =>
+ let val j = i + 1
+ in (j, j) end);
+ in next end;
+
end;