src/Pure/General/position.scala
changeset 56462 b64b0cb845fe
parent 55884 f2c0eaedd579
child 56464 555f4be59be6
--- a/src/Pure/General/position.scala	Tue Apr 08 10:24:42 2014 +0200
+++ b/src/Pure/General/position.scala	Tue Apr 08 12:19:33 2014 +0200
@@ -79,10 +79,15 @@
 
   object Reported
   {
-    def unapply(pos: T): Option[(Long, String, Symbol.Range)] =
+    def unapply(pos: T): Option[(Long, Command.Chunk.Name, Symbol.Range)] =
       (pos, pos) match {
         case (Id(id), Range(range)) =>
-          Some((id, File.unapply(pos).getOrElse(""), range))
+          val chunk_name =
+            pos match {
+              case File(name) => Command.Chunk.File_Name(name)
+              case _ => Command.Chunk.Self
+            }
+          Some((id, chunk_name, range))
         case _ => None
       }
   }