isabelle: src/Pure/Concurrent/counter.ML@40a3fc07a587 (annotated)

52537 4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	1	(* Title: Pure/Concurrent/counter.ML
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	2	Author: Makarius
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	3
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	4	Synchronized counter for unique identifiers > 0.
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	5
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	6	NB: ML ticks forwards, JVM ticks backwards.
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	7	*)
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	8
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	9	signature COUNTER =
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	10	sig
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	11	val make: unit -> unit -> int
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	12	end;
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	13
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	14	structure Counter: COUNTER =
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	15	struct
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	16
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	17	fun make () =
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	18	let
62920 a5853334c179 ensure globally unique counter results; wenzelm parents: 52537 diff changeset	19	val counter = Synchronized.var "counter" 0;
52537 4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	20	fun next () =
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	21	Synchronized.change_result counter
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	22	(fn i =>
68804 cbde6e3b132b actually ensure globally unique counter results (amending a5853334c179); wenzelm parents: 62920 diff changeset	23	let
cbde6e3b132b actually ensure globally unique counter results (amending a5853334c179); wenzelm parents: 62920 diff changeset	24	val k = i + 1;
cbde6e3b132b actually ensure globally unique counter results (amending a5853334c179); wenzelm parents: 62920 diff changeset	25	val n = if Thread_Data.is_virtual then 2 * k + 1 else 2 * k;
cbde6e3b132b actually ensure globally unique counter results (amending a5853334c179); wenzelm parents: 62920 diff changeset	26	in (n, k) end);
52537 4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	27	in next end;
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	28
4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: diff changeset	29	end;

author	paulson <lp15@cam.ac.uk>
	Wed, 24 Apr 2024 20:56:26 +0100
changeset 80149	40a3fc07a587
parent 68804	cbde6e3b132b
permissions	-rw-r--r--