Provide workspace symbols from Dafny LSP #4619
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Comments
dschoepe
added
the
kind: enhancement
keyboardDrummer
pushed a commit
that referenced
this issue
Oct 9, 2023
### 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 [#4619](#4619)
robin-aws
pushed a commit
to robin-aws/dafny
that referenced
this issue
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
Summary
By implementing the
workspace/symbolrequest, Dafny users can directly jump to declarations anywhere in their workspace, greatly simplifying file navigation in large projects.Background and Motivation
When working on large projects in other languages, I heavily rely on jumping directly to relevant definitions rather than remembering what file they are in. Generally, this feature would simplify interacting with large Dafny projects.
Many languages already provide this feature, which powers IDE operations such as "go to symbol" in VSCode. Since this request is part of the LSP standard, this support is straightforward to add.
Proposed Feature
By extending the Dafny LSP implementation through adding a handler for
workspace/symbolrequests, existing IDE features can directly make use of this functionality. Concretely, this can be done extendingWorkspaceSymbolsHandlerBaseand adding it the same way as other request handlers in the language server here.Alternatives
The easiest workaround is to use textual search to find where symbols are defined instead. However, this is less convenient to use as the user has to manually determine whether a textual match is a usage of a symbol or its definition site. While this can be worked around by using a regex that lists all the keywords for Dafny declarations (
function,predicate,class, etc.), this is more brittle than a language-aware solution as proposed here.This solution follows the same approach as other languages, i.e. by relying on the LSP standard.
The text was updated successfully, but these errors were encountered: