Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Return empty completions rather than error #1012

Merged
merged 1 commit into from
Jan 28, 2025

Conversation

Durbatuluk1701
Copy link
Contributor

I believe this should address the spamming of Request textDocument/completion failed errors that can be encountered on each character if a completion is not found when "vscoq.completion.enable": true.

This does not address anything about the underlying completion algorithm, rather just ensures that we can (almost) always return an empty list of possible completions.

I believe this is a more idiomatic way to implement completions (return either empty list or null) when no completions are available rather than a failure.

@rtetley
Copy link
Collaborator

rtetley commented Jan 28, 2025

Thanks a lot ! Does this close #989 ?

@Durbatuluk1701
Copy link
Contributor Author

Possibly? Not really sure what the root cause for crashes in #989 was as I’ve never encountered the language server crashing from the completions just giving lots of error messages.

@rtetley rtetley merged commit d5734a0 into coq:main Jan 28, 2025
28 checks passed
@Durbatuluk1701 Durbatuluk1701 deleted the empty_completion_management branch January 28, 2025 15:19
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants