changeset 55429 | 4a50f9e70dc1 |
parent 50201 | c26369c9eda6 |
child 55490 | 9b0fb0e2c9f5 |
--- a/src/Pure/General/position.scala Tue Feb 11 12:08:44 2014 +0100 +++ b/src/Pure/General/position.scala Tue Feb 11 15:05:13 2014 +0100 @@ -75,11 +75,12 @@ } } - object Id_Range + object Reported { - def unapply(pos: T): Option[(Long, Text.Range)] = + def unapply(pos: T): Option[(Long, String, Text.Range)] = (pos, pos) match { - case (Id(id), Range(range)) => Some((id, range)) + case (Id(id), Range(range)) => + Some((id, File.unapply(pos).getOrElse(""), range)) case _ => None } }