src/Pure/PIDE/document.scala
changeset 38355 8cb265fb12fe
parent 38227 6bbb42843b6e
child 38356 443fb83a21e8
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -16,11 +16,14 @@
     1.4  {
     1.5    /* formal identifiers */
     1.6  
     1.7 -  type Version_ID = String
     1.8 -  type Command_ID = String
     1.9 -  type State_ID = String
    1.10 +  type Version_ID = Long
    1.11 +  type Command_ID = Long
    1.12 +  type State_ID = Long
    1.13  
    1.14 -  val NO_ID = ""
    1.15 +  val NO_ID = 0L
    1.16 +
    1.17 +  def parse_id(s: String): Long = java.lang.Long.parseLong(s)
    1.18 +  def print_id(id: Long): String = id.toString
    1.19  
    1.20  
    1.21