diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Mon Mar 03 12:24:14 2014 +0100 +++ b/src/Pure/General/position.scala Mon Mar 03 12:54:12 2014 +0100 @@ -50,8 +50,8 @@ object Range { - def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop) - def unapply(pos: T): Option[Text.Range] = + def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop) + def unapply(pos: T): Option[Symbol.Range] = (pos, pos) match { case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop)) case (Offset(start), _) => Some(Text.Range(start, start + 1)) @@ -61,7 +61,7 @@ object Id_Offset { - def unapply(pos: T): Option[(Long, Text.Offset)] = + def unapply(pos: T): Option[(Long, Symbol.Offset)] = (pos, pos) match { case (Id(id), Offset(offset)) => Some((id, offset)) case _ => None @@ -70,7 +70,7 @@ object Def_Id_Offset { - def unapply(pos: T): Option[(Long, Text.Offset)] = + def unapply(pos: T): Option[(Long, Symbol.Offset)] = (pos, pos) match { case (Def_Id(id), Def_Offset(offset)) => Some((id, offset)) case _ => None @@ -79,7 +79,7 @@ object Reported { - def unapply(pos: T): Option[(Long, String, Text.Range)] = + def unapply(pos: T): Option[(Long, String, Symbol.Range)] = (pos, pos) match { case (Id(id), Range(range)) => Some((id, File.unapply(pos).getOrElse(""), range))