added general Synchronized.counter convenience;

--- 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;