Skip to content
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.

Sign up for GitHub

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

Jump to bottom

fix: make applyEdit optional in WorkspaceClientCapabilities of LSP #5224

Merged
merged 1 commit into from
Oct 16, 2024
Merged

fix: make applyEdit optional in WorkspaceClientCapabilities of LSP #5224

merged 1 commit into from
Oct 16, 2024

Conversation

pzread
Copy link
Contributor

@pzread pzread commented Sep 1, 2024 •
edited
Loading

The applyEdit field should be optional in WorkspaceClientCapabilities by the LSP spec and some clients don't populate it in requests

Closes #4541

@pzread pzread changed the title fix: make applyEdit optional in ClientCapabilities of LSP fix: make applyEdit optional in WorkspaceClientCapabilities of LSP Sep 1, 2024
@pzread
fix: make applyEdit optional in WorkspaceClientCapabilities of LSP
1d54f7b 
The `applyEdit` field should be optional in `WorkspaceClientCapabilities` by the
LSP spec and some clients don't populate it in requests

Closes leanprover#4541
@pzread
Copy link
Contributor Author

pzread commented Sep 1, 2024

The spec of applyEdit can be found in https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#clientCapabilities

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 1, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-08-31 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-09-01 10:36:42)

@pzread pzread marked this pull request as ready for review September 1, 2024 10:37
@pzread pzread requested a review from mhuisi as a code owner September 1, 2024 10:37
@pzread
Copy link
Contributor Author

pzread commented Sep 5, 2024

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Sep 5, 2024
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Sep 13, 2024
@mhuisi
Copy link
Contributor

mhuisi commented Oct 16, 2024

Thanks! Sorry for taking so long to merge this.

@mhuisi mhuisi added this pull request to the merge queue Oct 16, 2024
Merged via the queue into leanprover:master with commit b333de1 Oct 16, 2024
15 checks passed
@mhuisi mhuisi mentioned this pull request Oct 16, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mhuisi mhuisi mhuisi approved these changes

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Consider making WorkspaceClientCapabilities.applyEdit field Optionable
4 participants
@pzread @leanprover-community-mathlib4-bot @mhuisi @leanprover-bot