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.

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

Fix #3415 #3541

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Fix #3415 #3541

wants to merge 1 commit into from

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.

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