Fix: Automode button in Strategy Pane could not be used to stop automode

[unp1]

Intended Change

The automod ebutton in the strategy pane could no longer be used to stop an automode run as it was blocked by the glass pane which prevents interactions with a running proof. This PR enables the stopping feature again.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)

Ensuring quality

• I have tested the feature as follows: manual test

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[WolframPfeifer]

I can confirm the bug. Also, I think the button should somehow reflect the selection of the current strategy introduced by #3857. Alternatively, we could also think about removing it imo (I think I never used it until today).

Slightly related: The main "Play" button in the toolbar is a lot smaller now for me, making it less prominent and more difficult to click.
@mattulbrich Was that intentional?

[WolframPfeifer]

@mattulbrich Probably also related: The (non-destrictive) user actions, i.e. running macros/strategy, applying rules individually, loading a proof etc., used to be recorded (see class UserAction), to make it possible to undo them. This seems to be broken now for clicks on the main toolbar button.

[mattulbrich]

@unp1. Oh. I think I totally forgot about this button. I did not recall at all that there are two auto-play buttons. Thanks!

[unp1]

I agree we can remove the button, but for the button is at the moment a nice shortcut to restart the startegies on the whole tree instead of the seelected node.

Maybe we can have in the toolbar something like [Auto Button] o node o proof <-- supposed to be radio buttons
(or just ctrl-click on button == run on whole proof?)

[mattulbrich]

Slightly related: The main "Play" button in the toolbar is a lot smaller now for me, making it less prominent and more difficult to click.

I understand. Now it is like this: Not exactly beautiful ...

[mattulbrich]

[edited]. Now it is this ... that's ok

[mattulbrich]

@mattulbrich Probably also related: The (non-destrictive) user actions, i.e. running macros/strategy, applying rules individually, loading a proof etc., used to be recorded (see class UserAction), to make it possible to undo them. This seems to be broken now for clicks on the main toolbar button.

I see. I was not aware of this. Is this easy to lift by making the actions inherit from UserAction? Should not be too difficult. Or is there more to it?

[Also: UserActions could return an "undo callable", such that one can keep a list of these to undo more than one user action, but that is topic of a different pr.]

Also: perhaps it is better to bring back the original auto behaviour? Richard seems to miss it and the divergence to the other button is perhaps also not wanted.

[unp1]

Also: perhaps it is better to bring back the original auto behaviour? Richard seems to miss it and the divergence to the other button is perhaps also not wanted.

I would be actually just happy with a short cut like shift+click on button to run on the whole tree (I allowe dmyself to sneak that change into this PR, but we can of course drop it).

[WolframPfeifer]

I like the shift+click shortcut. Also, I just pushed a commit that repairs the undo feature (by delegating to the corresponding ProofMacroUserAction).

[unp1]

Hi all,
JFYI, I took the PR out of draft mode. I left the PR status at in progress in case some of you want still to make changes before going into review

[WolframPfeifer]

That is a collaborative PR with commits from @unp1, @mattulbrich, @WolframPfeifer. Maybe we should get an independent reviewer. @Drodt?