Skip to content
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

Feature Request: Go to Definition #4

Open
BoltonBailey opened this issue Jan 18, 2025 · 3 comments
Open

Feature Request: Go to Definition #4

BoltonBailey opened this issue Jan 18, 2025 · 3 comments

Comments

@BoltonBailey
Copy link

Nice extension!

I have a feature request, no idea of the effort required: When I click on the entry from the search results, it seems to insert the declaration name at my cursor. I would like if, instead, the extension could navigate me to the location of the declaration in the Mathlib installation for my project, similar to the "Go to Definition functionality" one gets by command-clicking, or if there were some kind of option for this in the menu.

@BoltonBailey BoltonBailey changed the title Feature Request: Feature Request: Go to Definition Jan 18, 2025
@Shreyas4991
Copy link
Owner

There are three buttons on the search result. The third one takes you to the mathlib docs

@Shreyas4991
Copy link
Owner

Ah I see you mean you want to open the source?

@Shreyas4991
Copy link
Owner

@BoltonBailey : I am a bit busy, and might get to it next month. But feel free to send a PR. I'll review and merge it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants