src/Pure/System/session.scala
changeset 38355 8cb265fb12fe
parent 38260 d4a1c7a19be3
child 38359 96b22dfeb56a
     1.1 --- a/src/Pure/System/session.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5    /* managed entities */
     1.6  
     1.7 -  type Entity_ID = String
     1.8 +  type Entity_ID = Long
     1.9  
    1.10    trait Entity
    1.11    {
    1.12 @@ -58,8 +58,12 @@
    1.13  
    1.14    /* unique ids */
    1.15  
    1.16 -  private var id_count: BigInt = 0
    1.17 -  def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
    1.18 +  private var id_count: Long = 0
    1.19 +  def create_id(): Session.Entity_ID = synchronized {
    1.20 +    require(id_count > java.lang.Long.MIN_VALUE)
    1.21 +    id_count -= 1
    1.22 +    id_count
    1.23 +  }
    1.24  
    1.25  
    1.26