src/Pure/PIDE/document.scala
changeset 43662 e3175ec00311
parent 43427 5c716a68931a
child 43697 77ce24aa1770
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Jul 04 22:11:32 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jul 04 22:25:33 2011 +0200
     1.3 @@ -27,7 +27,8 @@
     1.4    type Command_ID = ID
     1.5    type Exec_ID = ID
     1.6  
     1.7 -  val NO_ID: ID = 0
     1.8 +  val no_id: ID = 0
     1.9 +  val new_id = new Counter
    1.10  
    1.11  
    1.12  
    1.13 @@ -121,7 +122,7 @@
    1.14  
    1.15    object Version
    1.16    {
    1.17 -    val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
    1.18 +    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
    1.19    }
    1.20  
    1.21    class Version(val id: Version_ID, val nodes: Map[String, Node])