KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

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

Open WolframPfeifer opened 6 months ago

WolframPfeifer commented 6 months ago

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.