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.

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

Work around VS Code completion bug #1885

Merged
merged 1 commit into from
Nov 29, 2022
Merged

Conversation

Kha
Copy link
Member

@Kha Kha commented Nov 26, 2022

Builds on top of #1884
Fixes #1858

I consider this a clear bug on VS Code's part: microsoft/vscode#155738

(notFoundX := pure { items := #[], isIncomplete := true }) fun snap => do
(notFoundX :=
-- work around https://github.com/microsoft/vscode/issues/155738
pure { items := #[{label := "-"}], isIncomplete := true }) fun snap => do
Copy link
Member Author

@Kha Kha Nov 26, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that the the completion item should not be observable in practice as a follow-up didChange notification that should come with its own completion request must already be received to end up in this branch.

@gebner gebner force-pushed the vs-code-completion branch from 0ab2dca to e283a9a Compare November 28, 2022 23:59
src/Lean/Server/Requests.lean Outdated Show resolved Hide resolved
@Kha Kha force-pushed the vs-code-completion branch from e283a9a to f231d6b Compare November 29, 2022 12:34
@Kha Kha requested a review from gebner November 29, 2022 12:36
@gebner gebner merged commit bc0684a into leanprover:master Nov 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

No autocompletion when typing even number of characters in VSCode
2 participants