class Counter as abstract datatype;

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

--- 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()
 
 
 

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