src/Pure/PIDE/query_operation.scala
changeset 60893 3c8b9b4b577c
parent 57612 990ffb84489b
child 61206 d5aeb401111a
--- a/src/Pure/PIDE/query_operation.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -201,7 +201,7 @@
     for {
       command <- current_location
       snapshot = editor.node_snapshot(command.node_name)
-      link <- editor.hyperlink_command(snapshot, command)
+      link <- editor.hyperlink_command(true, snapshot, command)
     } link.follow(editor_context)
   }