Skip to content

Alternative for: "If possible save the last selected node in the proof, to reselect it upon loading."#3380

Draft
wadoon wants to merge 3 commits intomainfrom
weigl/restorelastnode
Draft

Alternative for: "If possible save the last selected node in the proof, to reselect it upon loading."#3380
wadoon wants to merge 3 commits intomainfrom
weigl/restorelastnode

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Dec 28, 2023

Alternative version for #3324 using the settings instead of storing it in the proof.

Using a path encoding of the current node (list of child indexes) and a run-length encoding to keep it small.

Missing: Finding the right spot where the KeYUserProblemFile is available and the proof is loaded. The current place is unsuitable.

@wadoon wadoon requested a review from unp1 December 28, 2023 04:13
@KeYProject KeYProject deleted a comment from codecov bot Feb 3, 2024
@wadoon wadoon marked this pull request as ready for review February 3, 2024 16:47
@wadoon
Copy link
Member Author

wadoon commented Feb 3, 2024

@unp1 I now call getMediator().nonGoalChosen(node) with a valid node, but it is not selected. Where is the other place with the logic that the last node should be taken?

@KeYProject KeYProject deleted a comment from codecov bot Feb 3, 2024
@wadoon wadoon self-assigned this Feb 9, 2024
@wadoon wadoon force-pushed the weigl/restorelastnode branch from 66b0aa4 to 5b1bd4d Compare June 29, 2025 23:00
@wadoon wadoon marked this pull request as draft June 29, 2025 23:01
@wadoon wadoon force-pushed the weigl/restorelastnode branch from 5b1bd4d to c9232c2 Compare September 7, 2025 23:04
@KeYProject KeYProject deleted a comment from codecov bot Sep 7, 2025
@wadoon wadoon force-pushed the weigl/restorelastnode branch from c9232c2 to 6a3c379 Compare September 10, 2025 20:55
@wadoon
Copy link
Member Author

wadoon commented Sep 10, 2025

@unp1 @mattulbrich I updated this to the latest main. The current obstacle is the lack of communication bandwidth, which prevents the provision of additional information to the UI world.

I can vaguely remember that we had a conclusion in Feb'2024 that the additional (KeY-/tool-maintained) information should be separated from \settings {}. Correct?

@wadoon wadoon added this to the v2.12.4 milestone Sep 10, 2025
@wadoon wadoon force-pushed the weigl/restorelastnode branch from 192b7fa to 48b5e70 Compare October 11, 2025 22:55
@wadoon wadoon modified the milestones: v2.13.0, v2.14.0 Nov 21, 2025
@wadoon wadoon modified the milestones: NextMajor, NextMinor Jan 13, 2026
@wadoon wadoon force-pushed the weigl/restorelastnode branch from 48b5e70 to 66b0aa4 Compare February 1, 2026 21:19
@codecov
Copy link

codecov bot commented Feb 1, 2026

Codecov Report

❌ Patch coverage is 67.93893% with 42 lines in your changes missing coverage. Please review.
✅ Project coverage is 37.93%. Comparing base (603b2ca) to head (66b0aa4).
⚠️ Report is 1699 commits behind head on main.

Files with missing lines Patch % Lines
.../uka/ilkd/key/proof/io/OutputStreamProofSaver.java 25.00% 14 Missing and 1 partial ⚠️
...core/src/main/java/de/uka/ilkd/key/proof/Node.java 0.00% 12 Missing ⚠️
...n/java/de/uka/ilkd/key/settings/Configuration.java 9.09% 10 Missing ⚠️
...uka/ilkd/key/macros/scripts/ProofScriptEngine.java 0.00% 2 Missing ⚠️
.../src/main/java/de/uka/ilkd/key/nparser/KeyAst.java 90.90% 1 Missing ⚠️
...de/uka/ilkd/key/proof/init/KeYUserProblemFile.java 75.00% 0 Missing and 1 partial ⚠️
...n/java/de/uka/ilkd/key/settings/ProofSettings.java 90.00% 1 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##               main    #3380    +/-   ##
==========================================
  Coverage     37.93%   37.93%            
- Complexity    17030    17038     +8     
==========================================
  Files          2060     2060            
  Lines        126300   126409   +109     
  Branches      21304    21324    +20     
==========================================
+ Hits          47913    47958    +45     
- Misses        72499    72560    +61     
- Partials       5888     5891     +3     

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

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@wadoon wadoon force-pushed the weigl/restorelastnode branch from 66b0aa4 to 48b5e70 Compare February 2, 2026 17:55
# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
@wadoon wadoon force-pushed the weigl/restorelastnode branch from 48b5e70 to f18f025 Compare February 2, 2026 18:01
@wadoon wadoon force-pushed the weigl/restorelastnode branch from f18f025 to a3cb671 Compare February 2, 2026 18:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant