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

Query in Error state #607

Open
rtetley opened this issue Sep 4, 2023 · 2 comments
Open

Query in Error state #607

rtetley opened this issue Sep 4, 2023 · 2 comments
Labels
bug Something isn't working prio:high
Milestone
Road map star issues

Comments

@rtetley
Copy link
Collaborator

rtetley commented Sep 4, 2023

Loosely related to #537
When performing a query while in error state (right after having executed a line with an error), queries do not work.
Searches return no results and other queries return no context found.
We need to get the correct state before launching the query in the backend
@rtetley rtetley added the bug Something isn't working label Sep 4, 2023
@nbrader
Copy link

nbrader commented Apr 23, 2024 •
edited
Loading

I'm unsure if it's related but I'm finding that with v2.1.2 running on Ubuntu, I'm not able to use the "Search" at all. Please refer to attached GIF as demonstration. It doesn't seem to have an issue with extra tabs: only the first tab does this.

Proof Assistant Query - Search Issue

@rtetley
Copy link
Collaborator Author

rtetley commented Apr 24, 2024

Thanks for your report ! I have actually found this bug and corrected it ! #763
It will make it in the next release !

@rtetley rtetley added this to the Road map star issues milestone Jan 20, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working prio:high
Projects
None yet
Milestone
Road map star issues
Development

No branches or pull requests
2 participants
@rtetley @nbrader