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) }