# HG changeset patch # User wenzelm # Date 1289335459 -3600 # Node ID 9c390868d2554507679019c87e78f0fa224af5e8 # Parent f9347a30d1b2abf30e292a471d2c1776110a9e81 added general Synchronized.counter convenience; diff -r f9347a30d1b2 -r 9c390868d255 src/Pure/Concurrent/synchronized.ML --- 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; diff -r f9347a30d1b2 -r 9c390868d255 src/Pure/Concurrent/synchronized_sequential.ML --- 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; diff -r f9347a30d1b2 -r 9c390868d255 src/Pure/PIDE/document.ML --- 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;