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.

Sign up for GitHub

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

Jump to bottom

Jump to definition #53

Closed
Alizter opened this issue Oct 7, 2022 · 2 comments · Fixed by #318
Closed

Jump to definition #53

Alizter opened this issue Oct 7, 2022 · 2 comments · Fixed by #318
Labels
kind: enhancement New feature or request part: lsp server part: protocol (LSP)
Milestone
0.1.5

Comments

@Alizter
Copy link
Collaborator

Alizter commented Oct 7, 2022

This will require libobject changes that @ejgallego was working on upstream in Coq. Should be straight forward to implement afterwards.
@ejgallego
Copy link
Owner

The upstream PR is ready to be tested here. Once we test it, we can merge it back to Coq.

@ejgallego ejgallego added this to the 0.1.1 milestone Nov 16, 2022
@ejgallego
Copy link
Owner

This requires a new Coq version so bumping milestone.

@ejgallego ejgallego modified the milestones: 0.1.1, 0.2.0 Dec 8, 2022
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[lsp] Basic jump to definition support.
a4f384c 
Due to lack of workspace metadata, this only works for the same file.

Fixes #53
@ejgallego ejgallego modified the milestones: 0.2.0, 0.1.5 Feb 14, 2023
This was referenced Feb 14, 2023
Closed
Merged
ejgallego added a commit that referenced this issue Feb 15, 2023
@ejgallego
[lsp] Basic jump to definition support.
ea72803 
Due to lack of workspace metadata, this only works for the same file.

Fixes #53
ejgallego added a commit that referenced this issue Feb 15, 2023
@ejgallego
[lsp] Basic jump to definition support.
03a88db 
Due to lack of workspace metadata, this only works for the same file.

Fixes #53
ejgallego added a commit that referenced this issue Feb 15, 2023
@ejgallego
[lsp] Basic jump to definition support.
dbd4e2e 
Due to lack of workspace metadata, this only works for the same file.

Fixes #53
ejgallego added a commit that referenced this issue Feb 15, 2023
@ejgallego
[lsp] Basic jump to definition support.
0108aaa 
Due to lack of workspace metadata, this only works for the same file.

Fixes #53
ejgallego added a commit that referenced this issue Feb 15, 2023
@ejgallego
[lsp] Basic jump to definition support.
3a1972b 
Due to lack of workspace metadata, this only works for the same file.

Fixes #53
@github-project-automation github-project-automation bot moved this from Todo to Done in coq-lsp roadmap Feb 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement New feature or request part: lsp server part: protocol (LSP)
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.5
Development

Successfully merging a pull request may close this issue.

[lsp] Basic jump to definition support. ejgallego/coq-lsp
2 participants
@ejgallego @Alizter