src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 16:20:42 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 17:04:29 2016 +0100
@@ -284,19 +284,7 @@
       : Option[Hyperlink] =
   {
     if (snapshot.is_outdated) None
-    else {
-      snapshot.state.find_command(snapshot.version, id) match {
-        case None => None
-        case Some((node, command)) =>
-          val name = command.node_name.node
-          val sources_iterator =
-            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-              (if (offset == 0) Iterator.empty
-               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-          val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
-          Some(hyperlink_file(focus, Line.Node_Position(name, pos)))
-      }
-    }
+    else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
   }
 
   def is_hyperlink_position(snapshot: Document.Snapshot,
@@ -304,7 +292,7 @@
   {
     pos match {
       case Position.Item_Id(id, offset) if offset > 0 =>
-        snapshot.state.find_command(snapshot.version, id) match {
+        snapshot.find_command(id) match {
           case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
             node.command_start(command) match {
               case Some(start) => text_offset == start + command.chunk.decode(offset)