changeset 38419 | f9dc924e54f8 |
parent 38417 | b8922ae21111 |
child 38423 | a9cff3f2e479 |
--- a/src/Pure/System/session.scala Sun Aug 15 18:41:23 2010 +0200 +++ b/src/Pure/System/session.scala Sun Aug 15 19:30:11 2010 +0200 @@ -49,7 +49,7 @@ /* unique ids */ private var id_count: Document.ID = 0 - def create_id(): Document.ID = synchronized { + def new_id(): Document.ID = synchronized { require(id_count > java.lang.Long.MIN_VALUE) id_count -= 1 id_count