# HG changeset patch
# User wenzelm
# Date 1482490411 -3600
# Node ID 5a2c15faf89ca27b476bfacf5072147ee7640dce
# Parent  84aea854dc3cf8f5c15272f97a9d462098fad664
tuned;

diff -r 84aea854dc3c -r 5a2c15faf89c 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)] =
diff -r 84aea854dc3c -r 5a2c15faf89c src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 11:36:41 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 11:53:31 2016 +0100
@@ -315,7 +315,7 @@
     text_offset: Text.Offset, pos: Position.T): Boolean =
   {
     pos match {
-      case Position.Id_Offset0(id, offset) if offset > 0 =>
+      case Position.Item_Id(id, offset) if offset > 0 =>
         snapshot.state.find_command(snapshot.version, id) match {
           case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
             node.command_start(command) match {
@@ -331,10 +331,9 @@
   def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
       : Option[Hyperlink] =
     pos match {
-      case Position.Line_File(line, name) =>
-        val offset = Position.Offset.unapply(pos) getOrElse 0
+      case Position.Item_File(name, line, offset) =>
         hyperlink_source_file(focus, name, line, offset)
-      case Position.Id_Offset0(id, offset) =>
+      case Position.Item_Id(id, offset) =>
         hyperlink_command_id(focus, snapshot, id, offset)
       case _ => None
     }
@@ -342,10 +341,9 @@
   def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
       : Option[Hyperlink] =
     pos match {
-      case Position.Def_Line_File(line, name) =>
-        val offset = Position.Def_Offset.unapply(pos) getOrElse 0
+      case Position.Item_Def_File(name, line, offset) =>
         hyperlink_source_file(focus, name, line, offset)
-      case Position.Def_Id_Offset0(id, offset) =>
+      case Position.Item_Def_Id(id, offset) =>
         hyperlink_command_id(focus, snapshot, id, offset)
       case _ => None
     }