# HG changeset patch # User wenzelm # Date 1319302803 -7200 # Node ID 27466646a7a3e9fa9ac5c2c1080616628be75198 # Parent 401f91ed8a93b7ece267a1f2661cae6fbb74be82 class Counter as abstract datatype; diff -r 401f91ed8a93 -r 27466646a7a3 src/Pure/Concurrent/counter.scala --- a/src/Pure/Concurrent/counter.scala Sat Oct 22 16:57:24 2011 +0200 +++ b/src/Pure/Concurrent/counter.scala Sat Oct 22 19:00:03 2011 +0200 @@ -12,9 +12,10 @@ object Counter { type ID = Long + def apply(): Counter = new Counter } -class Counter +class Counter private { private var count: Counter.ID = 0 diff -r 401f91ed8a93 -r 27466646a7a3 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Oct 22 16:57:24 2011 +0200 +++ b/src/Pure/PIDE/document.scala Sat Oct 22 19:00:03 2011 +0200 @@ -23,7 +23,7 @@ type Exec_ID = ID val no_id: ID = 0 - val new_id = new Counter + val new_id = Counter() diff -r 401f91ed8a93 -r 27466646a7a3 src/Pure/System/system_channel.scala --- a/src/Pure/System/system_channel.scala Sat Oct 22 16:57:24 2011 +0200 +++ b/src/Pure/System/system_channel.scala Sat Oct 22 19:00:03 2011 +0200 @@ -30,7 +30,7 @@ object Fifo_Channel { - private val next_fifo = new Counter + private val next_fifo = Counter() } class Fifo_Channel extends System_Channel