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

[unp1]

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

• 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)
• 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.
• I have tested the feature as follows: The steps for reproduction of Proof tree filters not applied correctly #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]

Codecov Report

All modified and coverable lines are covered by tests ✅

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

Additional details and impacted files

@@            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           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[WolframPfeifer]

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]

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]

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

see remark at #3367 (comment) instead

[WolframPfeifer]

I tested the GUI for the use cases that I could think of. Everything worked except the following minor bug: The selection highlights of expanded OSS nodes are not painted anymore (this worked in 2.12.0). The nodes are selected and the sequent is updated as expected (a feature implemented by @FliegendeWurst), just the selection highlight is not (it stays at the parent node).

[unp1]

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.

[WolframPfeifer]

Thanks! I tried to come up with the common use cases and tested them. Everything seems to work now.