Save and restore proof tree view filters upon proof switching

[unp1]

• Fix update of proof tree in case of filter changes (fixes Proof tree filters not applied correctly #3367)
• Store ProofTreeViewSettings per proof outside model and restore all settings upon switching

Related Issue

This pull request addresses #3367

The PR is an addition to the immediate bug fix PR #3368. It adds a new feature.

Intended Change

It removes some information from the GUIProofTreeModel that was kept redundant and only used for restoring the view state after proof switching.

The proof tree view states are now exported and saved explicitly thus allowing to also restore the filter settings on a per proof basis.

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: Opened different proofs with different filter settings and switching between them
• 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 (7a43f16) 37.96% compared to head (8da89ae) 37.98%.
Report is 10 commits behind head on main.

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3369      +/-   ##
============================================
+ Coverage     37.96%   37.98%   +0.01%     
- Complexity    17015    17024       +9     
============================================
  Files          2059     2059              
  Lines        126012   126029      +17     
  Branches      21281    21282       +1     
============================================
+ Hits          47845    47874      +29     
+ Misses        72282    72272      -10     
+ Partials       5885     5883       -2     

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

[unp1]

The latest push fixes a last bug I found when selecting two node filter in succession and removes some duplicate code. From my side (pending reviewer feedback), this PR is done (in case we want the feature)

[WolframPfeifer]

I can see pros and cons in having per-proof view filters. Somewhat recently, I had a discussion with @FliegendeWurst about this because he had a similar idea, and back then we decided not to make the filters proof dependent. Personally, I use the filters very often when working with KeY. I frequently switch between hidden/visible intermediate states (which roughly corresponds to the structure of the proof/detailed steps). In my opinion, it would be a bit annoying (in particular after reloading) if I had to set this option for each individual proof.

However, I would like to hear other opinions on this.

[unp1]

Hi,
I am fine with both semantics. But I would prefer this PR instead of the other:

• I can change it (easily) to preserve the old behavior (if that is preferred)
• this PR improves somewhat code quality and also the number of code lines (despite adding more comments)

[WolframPfeifer]

In our last KaKeY meeting, we decided to keep the current (non-local) filters, since (a) making them proof dependent would create a new category of settings (per-proof view settings) and (b) I prefer the filter settings to be global and basically no one else had a clear preference here.

@unp1 Can this PR be closed now?

[unp1]

Thanks!