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

Make the proof tree (or the KeY GUI in general) responsive during automatic proof search #3415

Open
WolframPfeifer opened this issue Feb 20, 2024 · 0 comments · May be fixed by #3541
Open
Labels
Feature New feature or request GUI

Comments

@WolframPfeifer
Copy link
Member

WolframPfeifer commented Feb 20, 2024

Idea

At the moment, during the automatic proof search the GUI of KeY "freezes", i.e. does not respond to input events except for a click on the stop button. However, depending on the step limit the automatic proof search might take quite a long time, in which the user can not do anything. It would be a very nice feature to be able to browse the proof (and maybe also other parts of the interface, for example the source code). While the proof search is ongoing, KeY should present the proof state from before the automatic search was started.

Additional context

Note that this feature request is probably not that easy to implement: The current solution for "freezing" the UI (except from the stop button) is to lay an invisible panel over the KeY GUI that blocks all clicks and input events. For this feature request, a different and more sophisticated solution will be needed.

@WolframPfeifer WolframPfeifer added GUI Feature New feature or request HacKeYthon Candidate Issue for HacKeYthon '25 labels Feb 20, 2024
@WolframPfeifer WolframPfeifer moved this to Candidate Issue in 2nd HacKeYthon Feb 20, 2024
@WolframPfeifer WolframPfeifer moved this to Candidate Issue in 3rd HacKeYthon Jan 31, 2025
wadoon added a commit that referenced this issue Feb 1, 2025
@wadoon wadoon linked a pull request Feb 1, 2025 that will close this issue
3 tasks
wadoon added a commit that referenced this issue Feb 8, 2025
@WolframPfeifer WolframPfeifer moved this from Candidate Issue to Selected in 3rd HacKeYthon Feb 10, 2025
@WolframPfeifer WolframPfeifer moved this from Selected to Group Topic Candidates in 3rd HacKeYthon Feb 14, 2025
@WolframPfeifer WolframPfeifer removed the HacKeYthon Candidate Issue for HacKeYthon '25 label Feb 14, 2025
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
Feature New feature or request GUI
Projects
Status: Candidate Issue
Development

Successfully merging a pull request may close this issue.

1 participant