fix: version numbers in code actions

[bustercopley]

Zulip topic

VS Code ignores the version number in a WorkspaceEdit but does not allow it to be null. There is at least one LSP client which does validate the version number, namely the Eglot client included in Emacs. By sending the correct version, we can be compatible with both.

This is a self-contained (std4-only) version, instead of the two changes (to lean4 and std4) that I mentioned on Zulip.

[bustercopley]

Fixed unused variable linter errors

[joehendrix]

@bustercopley Thanks, I'll find the right reviewer for this so we can figure out if it should belong in std or core.

[bustercopley]

Thanks!
Fixed long line linter error.

[david-christiansen]

From my reading of the spec, providing a null version means that the server has not yet heard of the file being open, rather than that the server simply doesn't want to send it, so this seems to strictly increase the conformance to the protocol.

[digama0]

This should be in Std.Lean, maybe Std.Lean.Lsp, ditto for textDocument

[mhuisi]

I think it may be better off in core as originally suggested by @bustercopley. Alternatively, if we keep it in std, we should delete ofTextEdit in core so that downstream users do not accidentally use the wrong function. I think I would personally prefer the former.

[digama0]

SGTM

[bustercopley]

Yes, especially since the changes to core amount to a simplificiation/streamlining, that is the natural place to do it. (I'm a bit intimidated by the process for core Lean PRs.)

[mhuisi]

Yes, especially since the changes to core amount to a simplificiation/streamlining, that is the natural place to do it. (I'm a bit intimidated by the process for core Lean PRs.)

It's fine to PR this without a corresponding RFC since it is very small, uncontroversial and you discussed it with the Lean community and the respective code owner :)

[bustercopley]

@mhuisi :) Do you mind saying something along those lines in the Zulip topic?

[bustercopley]

Force push: now depends on core #2721; squashed and rebased.