-
Notifications
You must be signed in to change notification settings - Fork 256
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
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
Milestone
Comments
This was referenced Jun 30, 2022
3 tasks
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
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 abreak;
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 methodsLocation? GetDeclaration(Position position)
andISet<Location> GetUsages(Position position)
, that can be and is available fromIdeState
. GetUsages can be used to implement "Find references"The text was updated successfully, but these errors were encountered: