--- 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;
--- a/src/Pure/Concurrent/synchronized_sequential.ML Tue Nov 09 21:13:06 2010 +0100
+++ b/src/Pure/Concurrent/synchronized_sequential.ML Tue Nov 09 21:44:19 2010 +0100
@@ -24,4 +24,15 @@
fun change var f = change_result var (fn x => ((), f x));
end;
+
+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;
--- a/src/Pure/PIDE/document.ML Tue Nov 09 21:13:06 2010 +0100
+++ b/src/Pure/PIDE/document.ML Tue Nov 09 21:44:19 2010 +0100
@@ -34,16 +34,7 @@
type exec_id = id;
val no_id = 0;
-
-local
- val id_count = Synchronized.var "id" 0;
-in
- fun new_id () =
- Synchronized.change_result id_count
- (fn i =>
- let val i' = i + 1
- in (i', i') end);
-end;
+val new_id = Synchronized.counter ();
val parse_id = Markup.parse_int;
val print_id = Markup.print_int;