src/Pure/General/position.scala
changeset 38355 8cb265fb12fe
parent 36683 41a1210519fd
child 38479 e628da370072
     1.1 --- a/src/Pure/General/position.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
     1.5    def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
     1.6    def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
     1.7 -  def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
     1.8 +  def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
     1.9  
    1.10    def get_range(pos: T): Option[(Int, Int)] =
    1.11      (get_offset(pos), get_end_offset(pos)) match {
    1.12 @@ -27,6 +27,6 @@
    1.13        case (None, _) => None
    1.14      }
    1.15  
    1.16 -  object Id { def unapply(pos: T): Option[String] = get_id(pos) }
    1.17 +  object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
    1.18    object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
    1.19  }