Fix update of proof tree in case of filter changes (fixes #3367)

unp1 commented 9 months ago

Related Issue

This pull request addresses #3367

Intended Change

Activating a filter works immediately.

The underlying problem is that the GUIProofTreeModel stores the selection and does not update with the selection model in the ProofTreeView.

This PR does not maintain the consistency. The redundant information was seemingly only thought to be used to store the selected node when switching proofs and restoring it when switching back. The method setFilter should for that reason not query the model for the selection but the view to get an up-to-date path.

Previously it got null (despite a node being selected in the view) and did not activate the filter.

Type of pull request

[x] Bug fix (non-breaking change which fixes an issue)
[ ] Refactoring (behaviour should not change or only minimally change)
[ ] New feature (non-breaking change which adds functionality)
[ ] Breaking change (fix or feature that would cause existing functionality to change)
[x] There are changes to the (Java) code
[ ] There are changes to the taclet rule base
[ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
[ ] Other:

Ensuring quality

[ ] I made sure that introduced/changed code is well documented (javadoc and inline comments).
[ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
[ ] I added new test case(s) for new functionality.
[x] I have tested the feature as follows: The steps for reproduction of #3367 do no longer reproduce the error. Playing around with multiple proofs and selecting filters seems to work.
[ ] I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

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

codecov[bot] commented 9 months ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Comparison is base (abbe1f8) 37.98% compared to head (e032871) 37.98%.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3368 +/- ## ========================================= Coverage 37.98% 37.98% Complexity 17024 17024 ========================================= Files 2059 2059 Lines 126029 126029 Branches 21282 21282 ========================================= Hits 47874 47874 Misses 72272 72272 Partials 5883 5883 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

WolframPfeifer commented 9 months ago

Thanks for the fast response! This PR fixes issue #3367. However, while testing the changes, I think I found another problem that is related (at the moment already present on main branch, but not before the merge of #3349): Changing the checkboxes in the "View" menu (Pretty printing, Unicode, Syntax Highlighting, ...) does not trigger a redraw. After a "manual" redraw (by switching nodes), the settings are applied correctly.

unp1 commented 9 months ago

I fixed the new issue in the other PR (but we can simply cherry-pick that commit if this PR should be used).

Previously the KeY's selection changed events were misused to cause updates of the GUI (but creating other problems) even so no other proof or node had been selected. The committed fix is not yet ideal, but the main window now redraws when pretty printer settings change. A proper solution would use the ChangeListener (or something similar like moving these changes to the Config class).

unp1 commented 9 months ago

~~I moved the refactoring (and bugfixes) from #3369 to here, but this PR keeps the old non-local filter semantics~~

see remark at https://github.com/KeYProject/key/issues/3367#issuecomment-1837080378 instead

unp1 commented 9 months ago

Thanks. The highlighting is fixed. It fixes also an exception, if a filter like "Hide Closed Subtrees" is activated, while an OSS child node is selected. The force push was just a rebase on the current main.

KeYProject / key