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

Support the "Find references" LSP request #2320

Closed
keyboardDrummer opened this issue Jun 29, 2022 · 0 comments · Fixed by #4271
Closed

Support the "Find references" LSP request #2320

keyboardDrummer opened this issue Jun 29, 2022 · 0 comments · Fixed by #4271
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) status: planned The team is planning to work on this in the near future

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jun 29, 2022

Support this LSP request type: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_references

Prerequisites

Implementation hints

AST Nodes can implement IHasUsages which allow them to report which declarations their references resolved to. For example a break; statement reports a usage to the loop which it is breaking out of, and as such you can ctrl+click on a break to jump to the loop.

An IdentifierExpr reports a usage to the variable which it points to.

The IHasUsages ASTNodes are used to create a SymbolTable which already has methods Location? GetDeclaration(Position position) and ISet<Location> GetUsages(Position position), that can be and is available from IdeState. GetUsages can be used to implement "Find references"

@cpitclaudel cpitclaudel added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) status: planned The team is planning to work on this in the near future labels Jun 29, 2022
@keyboardDrummer keyboardDrummer added this to the Project aware IDE milestone Jun 30, 2022
@alex-chew alex-chew self-assigned this May 30, 2023
keyboardDrummer added a commit that referenced this issue Jul 25, 2023
Fixes #2320.

- [x] Implement basic functionality
- [x] Add tests (WIP)
- [x] Update release notes

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Remy Willems <[email protected]>
keyboardDrummer added a commit to keyboardDrummer/dafny that referenced this issue Sep 15, 2023
Fixes dafny-lang#2320.

- [x] Implement basic functionality
- [x] Add tests (WIP)
- [x] Update release notes

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Remy Willems <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) status: planned The team is planning to work on this in the near future
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants