[LSP] Add handler for workspace/symbol requests [#4619] #4620
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
dschoepe
force-pushed
the
support-workspace-symbol-query
branch
from
1a36c16
to
910a427
Compare
dschoepe
force-pushed
the
support-workspace-symbol-query
branch
from
910a427
to
1dc7ed5
Compare
This implements a response for workspace/symbol queries as documented here: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspace_symbol This allows jumping to symbols by name across a workspace (e.g. in VSCode, typing `#foo` in the navigation prompt allows jumping to an identifier containing foo as a substring). By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
dschoepe
force-pushed
the
support-workspace-symbol-query
branch
from
1dc7ed5
to
ebeaf57
Compare
| @@ -46,6 +46,18 @@ | |||
| <None Update="Lookup\TestFiles\find-refs-b.dfy"> | |||
| <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory> | |||
| </None> | |||
| <None Update="Lookup\TestFiles\defines-foo.dfy"> | |||
There was a problem hiding this comment.
My preference is for the test files to be inline in the tests. This is similar to what Roslyn's (C# compiler) tests look like. I don't have a good argument for one or the other though, so feel free to ignore this comment.
There was a problem hiding this comment.
I was followed this approach based on ReferencesTest but I'm fine either way. I'll update the PR and inline them instead.
keyboardDrummer
requested changes
Oct 6, 2023
Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs
Outdated
Show resolved
Hide resolved
| public override async Task<Container<SymbolInformation>?> Handle(WorkspaceSymbolParams request, CancellationToken cancellationToken) { | ||
| var queryText = request.Query.ToLower(); | ||
| Dictionary<SymbolInformation, int> result = new Dictionary<SymbolInformation, int>(); | ||
| // Using a LINQ traversal here would be more readable, but to be as responsive |
There was a problem hiding this comment.
I think the code makes it clear that LINQ can't be used, so IMO the comment is unnecessary.
There was a problem hiding this comment.
Sounds good, I'll remove that.
| // as it includes things like keywords and the signature of the | ||
| // the definitions. However, extracting just the name from | ||
| // an ISymbol requires explicit case splitting for each definition | ||
| var description = def.GetDescription(dafnyOptions); |
There was a problem hiding this comment.
Wouldn't def.NameToken.val give you the name?
Also, this doesn't match on qualified names, does it? (could be a future feature)
There was a problem hiding this comment.
Oh, I must have missed that. I'll change it. Good callout about the qualified names. I'll leave a note here about it.
Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs
Outdated
Show resolved
Hide resolved
Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs
Outdated
Show resolved
Hide resolved
Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs
Outdated
Show resolved
Hide resolved
Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs
Outdated
Show resolved
Hide resolved
keyboardDrummer
previously approved these changes
Oct 9, 2023
keyboardDrummer
approved these changes
Oct 9, 2023
robin-aws
pushed a commit
to robin-aws/dafny
that referenced
this pull request
Oct 11, 2023
…fny-lang#4620) ### Description This implements a response for workspace/symbol queries as documented here: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspace_symbol This allows jumping to symbols by name across a workspace (e.g. in VSCode, typing `#foo` in the navigation prompt allows jumping to an identifier containing foo as a substring). By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. ### How has this been tested - Added unit tests in DafnyLanguageServer.Test. - Manually tested on some projects. Addresses [dafny-lang#4619](dafny-lang#4619)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
This implements a response for workspace/symbol queries as documented here:
https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspace_symbol
This allows jumping to symbols by name across a workspace (e.g. in VSCode, typing
#fooin the navigation prompt allows jumping to an identifier containing foo as a substring).By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
How has this been tested
Addresses #4619