feat: LSP rename support #4365
feat: LSP rename support #4365
Conversation
# Conflicts: # Source/DafnyLanguageServer/Workspace/SymbolTable.cs
| // Reject rename requests in implicit projects, because we might not find all references within the codebase, | ||
| // so a partial rename may result in breaking the codebase | ||
| if ((await projects.GetProject(requestUri)).IsImplicitProject) { | ||
| throw new Exception("Renaming support requires --project-mode and a Dafny project file (dfyconfig.toml)"); |
There was a problem hiding this comment.
What's the resulting behavior in the client? Does it allow the user to attempt to rename after which nothing happens, or it the rename prevented altogether?
I see that LSP also has a prepareRename request: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_prepareRename
that seems to be meant to deal with situations in which renaming is not valid, but that doesn't seem to be implemented here.
There was a problem hiding this comment.
What's the resulting behavior in the client? Does it allow the user to attempt to rename after which nothing happens, or it the rename prevented altogether?
The VS Code client prevents the rename altogether, making no document changes, and shows the error message of the exception. Unfortunately, the Omnisharp library doesn't seem to have a way to cleanly show an error message, so the error message looks like a crash (includes stack trace and everything) until you read the message in detail. If there's a better way to display an error message, please let me know.
I see that LSP also has a prepareRename request: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_prepareRename
that seems to be meant to deal with situations in which renaming is not valid, but that doesn't seem to be implemented here.
Indeed this PR doesn't implement the prepareRename request.
|
Looks great! Left one comment |
| public async Task RenameNonSymbolFails() { | ||
| var tempDir = await SetUpProjectFile(); | ||
| var documentItem = await CreateAndOpenTestDocument("module Foo {}", Path.Combine(tempDir, "tmp.dfy")); | ||
| var workspaceEdit = await RequestRename(documentItem, new Position(0, 6), "space"); |
There was a problem hiding this comment.
What if you do a PrepareRename call here? Can that one fail and succeed?
Fixes #2322.
TODO:
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.