Feature: If possible save the last selected node in the proof, to reselect it upon loading.

[unp1]

This commit addresses issue #3297.

[codecov]

Codecov Report

Attention: 40 lines in your changes are missing coverage. Please review.

Comparison is base (ac66700) 37.86% compared to head (638e108) 37.85%.

Files	Patch %	Lines
...of/io/IntermediatePresentationProofFileParser.java	31.25%	11 Missing ⚠️
.../uka/ilkd/key/proof/io/OutputStreamProofSaver.java	25.00%	8 Missing and 1 partial ⚠️
...a/ilkd/key/proof/io/IntermediateProofReplayer.java	33.33%	5 Missing and 1 partial ⚠️
...e/uka/ilkd/key/proof/io/AbstractProblemLoader.java	37.50%	2 Missing and 3 partials ⚠️
...key/proof/io/intermediate/AppNodeIntermediate.java	33.33%	4 Missing ⚠️
...ore/src/main/java/de/uka/ilkd/key/proof/Proof.java	0.00%	2 Missing ⚠️
...main/java/de/uka/ilkd/key/proof/io/ProofSaver.java	60.00%	2 Missing ⚠️
.../main/java/de/uka/ilkd/key/proof/io/AutoSaver.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3324      +/-   ##
============================================
- Coverage     37.86%   37.85%   -0.01%     
- Complexity    16905    16908       +3     
============================================
  Files          2055     2055              
  Lines        125528   125553      +25     
  Branches      21226    21237      +11     
============================================
+ Hits          47525    47528       +3     
- Misses        72152    72171      +19     
- Partials       5851     5854       +3     

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

[wadoon]

Why does this have so many changed files. This should rather be a local feature.

Is it not possible to use the local settings, instead of the proof replayer?

[unp1]

Why does this have so many changed files. This should rather be a local feature.

The amount of files is just because we need to pass the selected node to the proof saver.

Is it not possible to use the local settings, instead of the proof replayer?

Sadly not as we do no save unique node identifiers in our proofs and the node numbers upon reload may differ (e.g. when the proof was pruned at some point).

[wadoon]

Sadly not as we do no save unique node identifiers in our proofs and the node numbers upon reload may differ (e.g. when the proof was pruned at some point).

Sarah and I have used a slightly different system to identify nodes uniquely. We used the path from root to the node in the same manner as PiO and PiS. See here. Of course, if you apply run-length encoding you can save a lot of entries in the list (mostly zero, and some ones).

[unp1]

I close this PR as we will fix the issue using #3380