Skip to content

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

Closed
wadoon wants to merge 2 commits intomainfrom
weigl/fix3415
Closed

Make the proof tree (or the KeY GUI in general) responsive during automatic proof search#3541
wadoon wants to merge 2 commits intomainfrom
weigl/fix3415

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Feb 1, 2025

Fixes #3415.

State:

  • Glasspane removed
  • KeyAction classes extended for enabledness updates
  • Look through actions and decide whether they are safe or not to be executed during auto-mode.

@wadoon wadoon added the GUI label Feb 1, 2025
@wadoon wadoon added this to the v2.12.4 milestone Feb 1, 2025
@wadoon wadoon self-assigned this Feb 1, 2025
@wadoon
Copy link
Member Author

wadoon commented Feb 6, 2025

State of this PR:

In this PR the GlassPane blocking the user input was removed. Instead of this overall deactivation, each action must be de-/activated. A new facility was introduced to KeyAction. KeyAction holds a predicate function () -> Boolean which defines its enability. KeyAction#updateEnabledness updates Action#setEnable accordingly to this function. This method should be used in listeners (property change listeners, etc...) to update the value.

MainWindowAction exploits this facility with two methods, which setup the listener and predicate function accordingly:

  • #enabledOnAnActiveProof();: Action is enabled if a proof is selected
  • #enabledWhenNotInAutoMode();: Action is not enabled if the main window is in "auto mode".

It is possible to call both methods, then the condition is conjunctively joint.

Note, that this PR requires manual testing and clicking within the GUI.

@wadoon wadoon changed the title Fix #3415 Make the proof tree (or the KeY GUI in general) responsive during automatic proof search Feb 28, 2025
@wadoon wadoon force-pushed the weigl/fix3415 branch 2 times, most recently from 4aebcdf to cc3a82d Compare August 29, 2025 11:53
@wadoon wadoon marked this pull request as ready for review August 29, 2025 11:54
@wadoon wadoon requested a review from unp1 August 29, 2025 11:54
@wadoon
Copy link
Member Author

wadoon commented Oct 11, 2025

Review requested for two months. I rebased and fixed formatting to finally abandon this PR.

@mattulbrich @unp1

@wadoon wadoon closed this Oct 11, 2025
@wadoon wadoon removed the request for review from unp1 October 11, 2025 22:59
@wadoon wadoon removed their assignment Oct 11, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

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

1 participant