New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(widget): add go to definition button. #3982
Conversation
Now you can hit a new button in the tooltip and it will reveal the definition location in the editor!
It's using |
There's no chance we could get ctrl+click with underline on ctrl+hover like in the editor, right? 😄 |
If -- you can't go to foo atm
def foo := 5
example : foo = foo := begin end |
ctrl+click could be done in theory but it would require some plumbing in core lean. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Otherwise lgtm.
bors d+
✌️ EdAyers can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
bors r+ |
Canceled. |
bors merge |
Now you can hit a new button in the tooltip and it will reveal the definition location in the editor! Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Now you can hit a new button in the tooltip and it will reveal the definition location in the editor! Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
Now you can hit a new button in the tooltip and it will reveal the definition location in the editor! Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>
Now you can hit a new button in the tooltip and it will reveal the definition location in the editor!