# HG changeset patch
# User wenzelm
# Date 1482506442 -3600
# Node ID 951507563033690d8bdfeab1d6c7fe200cc7ba1e
# Parent  4c9fb4d4bca3cf3be23f204ea19cc1739b38481c
tuned;

diff -r 4c9fb4d4bca3 -r 951507563033 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Pure/PIDE/editor.scala	Fri Dec 23 16:20:42 2016 +0100
@@ -28,7 +28,7 @@
     def follow(context: Context): Unit
   }
   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]
 }
 
diff -r 4c9fb4d4bca3 -r 951507563033 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Fri Dec 23 16:20:42 2016 +0100
@@ -208,7 +208,7 @@
     for {
       command <- state.location
       snapshot = editor.node_snapshot(command.node_name)
-      link <- editor.hyperlink_command(true, snapshot, command)
+      link <- editor.hyperlink_command(true, snapshot, command.id)
     } link.follow(editor_context)
   }
 
diff -r 4c9fb4d4bca3 -r 951507563033 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala	Fri Dec 23 16:20:42 2016 +0100
@@ -51,7 +51,7 @@
               case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
                 val link =
                   props match {
-                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(true, snapshot, id)
+                    case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
                     case _ => None
                   }
                 GUI_Thread.later {
diff -r 4c9fb4d4bca3 -r 951507563033 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
     }
 }
diff -r 4c9fb4d4bca3 -r 951507563033 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Dec 23 16:20:42 2016 +0100
@@ -96,7 +96,7 @@
     def print: String =
       "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
     def follow(snapshot: Document.Snapshot)
-    { PIDE.editor.hyperlink_command(true, snapshot, command).foreach(_.follow(view)) }
+    { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
   }