src/Pure/PIDE/query_operation.scala
changeset 64664 951507563033
parent 63805 c272680df665
child 65195 ffab6f460a82
--- 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)
   }