src/Pure/General/position.scala

--- a/src/Pure/General/position.scala	Fri Dec 23 11:36:41 2016 +0100
+++ b/src/Pure/General/position.scala	Fri Dec 23 11:53:31 2016 +0100
@@ -64,7 +64,7 @@
       }
   }
 
-  object Id_Offset0
+  object Item_Id
   {
     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
       pos match {
@@ -73,7 +73,7 @@
       }
   }
 
-  object Def_Id_Offset0
+  object Item_Def_Id
   {
     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
       pos match {
@@ -82,6 +82,28 @@
       }
   }
 
+  object Item_File
+  {
+    def unapply(pos: T): Option[(String, Int, Symbol.Offset)] =
+      pos match {
+        case Line_File(line, name) =>
+          val offset = Position.Offset.unapply(pos) getOrElse 0
+          Some((name, line, offset))
+        case _ => None
+      }
+  }
+
+  object Item_Def_File
+  {
+    def unapply(pos: T): Option[(String, Int, Symbol.Offset)] =
+      pos match {
+        case Def_Line_File(line, name) =>
+          val offset = Position.Def_Offset.unapply(pos) getOrElse 0
+          Some((name, line, offset))
+        case _ => None
+      }
+  }
+
   object Identified
   {
     def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =