src/Pure/General/position.scala
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
       }
   }