src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 16:20:42 2016 +0100
@@ -280,14 +280,14 @@
   }
 
   override def hyperlink_command(
-    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink] =
   {
     if (snapshot.is_outdated) None
     else {
-      snapshot.state.find_command(snapshot.version, command.id) match {
+      snapshot.state.find_command(snapshot.version, id) match {
         case None => None
-        case Some((node, _)) =>
+        case Some((node, command)) =>
           val name = command.node_name.node
           val sources_iterator =
             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
@@ -299,16 +299,6 @@
     }
   }
 
-  def hyperlink_command_id(
-    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
-      : Option[Hyperlink] =
-  {
-    snapshot.state.find_command(snapshot.version, id) match {
-      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
-      case None => None
-    }
-  }
-
   def is_hyperlink_position(snapshot: Document.Snapshot,
     text_offset: Text.Offset, pos: Position.T): Boolean =
   {
@@ -332,7 +322,7 @@
       case Position.Item_File(name, line, offset) =>
         hyperlink_source_file(focus, name, line, offset)
       case Position.Item_Id(id, offset) =>
-        hyperlink_command_id(focus, snapshot, id, offset)
+        hyperlink_command(focus, snapshot, id, offset)
       case _ => None
     }
 
@@ -342,7 +332,7 @@
       case Position.Item_Def_File(name, line, offset) =>
         hyperlink_source_file(focus, name, line, offset)
       case Position.Item_Def_Id(id, offset) =>
-        hyperlink_command_id(focus, snapshot, id, offset)
+        hyperlink_command(focus, snapshot, id, offset)
       case _ => None
     }
 }