KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Save and restore proof tree view filters upon proof switching #3369

Closed unp1 closed 9 months ago

unp1 commented 9 months ago

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

Ensuring quality

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 (7a43f16) 37.96% compared to head (8da89ae) 37.98%. Report is 10 commits behind head on main.

Additional details and impacted files ```diff @@ 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 ```

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

unp1 commented 9 months ago

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 commented 9 months ago

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 commented 9 months ago

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

WolframPfeifer commented 9 months ago

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 commented 9 months ago

Thanks!