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

Error message when the extension is not ready yet #36

Open
fpoli opened this issue Jan 12, 2021 · 0 comments
Open

Error message when the extension is not ready yet #36

fpoli opened this issue Jan 12, 2021 · 0 comments
Labels
enhancement New feature or request good-first-issue Good for newcomers

Comments

@fpoli
Copy link
Member

fpoli commented Jan 12, 2021

When a user tries to run a command like prusti-assistant.verify before the extension has been fully initialized, nothing happens and no error message is shown. This is confusing for the user.

We could improve the experience by registering early in activate() a dummy function for all the commands. The dummy function should just show a message that asks the user to wait for the full initialization of the extension.
@fpoli fpoli added enhancement New feature or request good-first-issue Good for newcomers labels Jan 12, 2021
@fpoli fpoli changed the title Error message when the extension is not yet ready Error message when the extension is not ready yet Jan 12, 2021
@fpoli fpoli mentioned this issue Dec 2, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request good-first-issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@fpoli