-
Notifications
You must be signed in to change notification settings - Fork 24
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Save and restore proof tree view filters upon proof switching #3369
Conversation
Codecov ReportAll modified and coverable lines are covered by tests ✅
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. |
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) |
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. |
Hi,
|
e9596b2
to
ce27480
Compare
f0c7433
to
0245d70
Compare
0245d70
to
22711b5
Compare
Each view setting update caused it own redraw even if itself did not change.
…tered correctly only for changes of interest
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? |
Thanks! |
* origin/main: (25 commits) bug fix applying spotless Configurable enabled keys for JML condition evaluation Spotless cleanups Fix selection highlight for OSS node child Remove unnecessary checks for correct change as listener is now registered correctly only for changes of interest Make usage of PropertyChangeListeners working (addendum to previous commit) Reduce number of sequentview updates Remove duplicate update of sequentview USe refactorings from KeYProject#3369 but preserve non-local filter semantics for proof tree view MainWindow updates sequent view after settings change for pretty printing Minor clean up to slightly simplify complexity of path selection in ProofTreeView Fix problem with closed subtree filter Fix node filter selection display in popup dialoh and some refactoring Restore correct node selection and remove unused fields from GUIProofTreeModel Store ProofTreeViewSettings per proof outside model and restore all settings upon switching Fix update of proof tree in case of filter changes (fixes KeYProject#3367) applying spotless Bump com.miglayout:miglayout-swing from 11.2 to 11.3 Configurable enabled keys for JML condition evaluation ...
* origin/main: (25 commits) bug fix applying spotless Configurable enabled keys for JML condition evaluation Spotless cleanups Fix selection highlight for OSS node child Remove unnecessary checks for correct change as listener is now registered correctly only for changes of interest Make usage of PropertyChangeListeners working (addendum to previous commit) Reduce number of sequentview updates Remove duplicate update of sequentview USe refactorings from #3369 but preserve non-local filter semantics for proof tree view MainWindow updates sequent view after settings change for pretty printing Minor clean up to slightly simplify complexity of path selection in ProofTreeView Fix problem with closed subtree filter Fix node filter selection display in popup dialoh and some refactoring Restore correct node selection and remove unused fields from GUIProofTreeModel Store ProofTreeViewSettings per proof outside model and restore all settings upon switching Fix update of proof tree in case of filter changes (fixes #3367) applying spotless Bump com.miglayout:miglayout-swing from 11.2 to 11.3 Configurable enabled keys for JML condition evaluation ... # Conflicts: # key.ui/build.gradle
* origin/main: (2237 commits) Bump org.slf4j:slf4j-api from 2.0.10 to 2.0.11 Bump org.slf4j:slf4j-api from 2.0.9 to 2.0.10 spotless after discussion: all datatypes are free ignore files in */antlr4/gen/* bug fix applying spotless Configurable enabled keys for JML condition evaluation Spotless cleanups Fix selection highlight for OSS node child Remove unnecessary checks for correct change as listener is now registered correctly only for changes of interest Make usage of PropertyChangeListeners working (addendum to previous commit) Reduce number of sequentview updates Remove duplicate update of sequentview USe refactorings from #3369 but preserve non-local filter semantics for proof tree view MainWindow updates sequent view after settings change for pretty printing Minor clean up to slightly simplify complexity of path selection in ProofTreeView Fix problem with closed subtree filter Fix node filter selection display in popup dialoh and some refactoring Restore correct node selection and remove unused fields from GUIProofTreeModel ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java # key/key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java # key/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java # key/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java # key/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java # key/key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java # key/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # key/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java # key/key.util/src/main/java/org/key_project/util/collection/Immutables.java
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.