Skip to content

(LSP) Include document version in code action [merged into nightly-testing]#7812

Merged
kim-em merged 2 commits intonightly-testingfrom
richard-copley/code-action-document-version
Oct 25, 2023
Merged

(LSP) Include document version in code action [merged into nightly-testing]#7812
kim-em merged 2 commits intonightly-testingfrom
richard-copley/code-action-document-version

Conversation

@bustercopley
Copy link
Copy Markdown
Contributor

@bustercopley bustercopley commented Oct 21, 2023 •
edited
Loading

  • WorkspaceEdit.ofTextEdit now takes a VersionedTextDocumentIdentifier instead of a URI
  • Use the new function EditableDocument.versionedIdentifier to get a VersionedTextDocumentIdentifier

See the Zulip topic and the two PRs below for further details.

  • Depends on core Lean 4 #2721
  • Depends on Std #306

Open in Gitpod

@bustercopley bustercopley added the blocked-by-core-PR This PR depends on a PR to Core/Std label Oct 21, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 21, 2023
@bustercopley bustercopley force-pushed the richard-copley/code-action-document-version branch from 6e02be9 to 7504888 Compare October 21, 2023 14:45
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 21, 2023
bustercopley added a commit that referenced this pull request Oct 21, 2023
@bustercopley
Update dependencies for CI (do not merge)
400cc88 
For Mathlib #7812 dependency on core #2721 and std #306
* lean-toolchain: leanprover/lean4-pr-releases:pr-release-2721
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
@bustercopley bustercopley changed the base branch from master to nightly-testing October 21, 2023 15:43
bustercopley added a commit that referenced this pull request Oct 21, 2023
@bustercopley
Update dependencies for CI (do not merge)
d8d37cc 
For Mathlib #7812 dependency on core #2721 and std #306
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
@bustercopley bustercopley force-pushed the richard-copley/code-action-document-version branch from 400cc88 to d8d37cc Compare October 21, 2023 16:35
@bustercopley bustercopley changed the base branch from nightly-testing to lean-pr-testing-2721 October 21, 2023 16:36
@bustercopley bustercopley force-pushed the richard-copley/code-action-document-version branch from d8d37cc to 400cc88 Compare October 22, 2023 01:47
bustercopley added a commit that referenced this pull request Oct 22, 2023
@bustercopley
Update dependencies for CI (do not merge)
6a3c135 
For Mathlib #7812 dependency on core #2721 and std #306
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
@bustercopley bustercopley force-pushed the richard-copley/code-action-document-version branch from 400cc88 to 6a3c135 Compare October 22, 2023 02:00
leanprover-community-mathlib4-bot and others added 2 commits October 22, 2023 10:32
@bustercopley
Update dependencies for CI (do not merge)
3665052 
For Mathlib #7812 dependency on core #2721 and std #306
* lean-toolchain: leanprover/lean4-pr-releases:pr-release-2721
* lakefile.lean: get std from the #306 branch
* lake-manifest.json: lake update
@bustercopley
fix: version numbers in code actions
fe763ae
@bustercopley bustercopley force-pushed the richard-copley/code-action-document-version branch from 6a3c135 to fe763ae Compare October 22, 2023 09:35
@bustercopley bustercopley changed the base branch from lean-pr-testing-2721 to nightly-testing October 22, 2023 09:36
@kim-em kim-em added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 22, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 23, 2023
@kim-em kim-em changed the title (LSP) Include document version in code action (LSP) Include document version in code action [merged into nightly-testing] Oct 25, 2023
@kim-em kim-em merged commit 93fc878 into nightly-testing Oct 25, 2023
@bors bors bot deleted the richard-copley/code-action-document-version branch October 25, 2023 09:44
This was referenced Feb 17, 2026
Closed
Closed
Closed
Closed
Closed
@github-actions github-actions bot mentioned this pull request Mar 1, 2026
Closed
@github-actions github-actions bot mentioned this pull request Mar 23, 2026
Closed
@github-actions github-actions bot mentioned this pull request Apr 2, 2026
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. blocked-by-core-PR This PR depends on a PR to Core/Std merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@bustercopley @kim-em