diff -r cc7a1285693f -r 3c8b9b4b577c src/Pure/PIDE/query_operation.scala --- 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) }