src/Pure/General/position.scala
changeset 57931 4e2cbff02f23
parent 57911 dcb758188aa6
child 59671 9715eb8e9408
     1.1 --- a/src/Pure/General/position.scala	Wed Aug 13 20:43:19 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Wed Aug 13 22:29:43 2014 +0200
     1.3 @@ -63,20 +63,20 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  object Id_Offset
     1.8 +  object Id_Offset0
     1.9    {
    1.10      def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    1.11 -      (pos, pos) match {
    1.12 -        case (Id(id), Offset(offset)) => Some((id, offset))
    1.13 +      pos match {
    1.14 +        case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
    1.15          case _ => None
    1.16        }
    1.17    }
    1.18  
    1.19 -  object Def_Id_Offset
    1.20 +  object Def_Id_Offset0
    1.21    {
    1.22      def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    1.23 -      (pos, pos) match {
    1.24 -        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
    1.25 +      pos match {
    1.26 +        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
    1.27          case _ => None
    1.28        }
    1.29    }