Provide workspace symbols from Dafny LSP

[dschoepe]

Summary

By implementing the workspace/symbol request, 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/symbol requests, existing IDE features can directly make use of this functionality. Concretely, this can be done extending WorkspaceSymbolsHandlerBase and 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.