This commit addresses issue #3297. Feature: If possible save the last selected node in the proof, to reselect it upon loading.

Author: unp1

key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java

@@ -1678,7 +1678,7 @@ protected void assertSaveAndReload(File baseDir, String javaPathInBaseDir,
         KeYEnvironment<DefaultUserInterfaceControl> reloadedEnv = null;
         SymbolicExecutionTreeBuilder reloadedBuilder = null;
         try {
-            ProofSaver saver = new ProofSaver(env.getProof(), tempFile.getAbsolutePath(),
+            ProofSaver saver = new ProofSaver(env.getProof(), null, tempFile.getAbsolutePath(),
                 KeYConstants.INTERNAL_VERSION);
             assertNull(saver.save());
             // Load proof from saved *.proof file

key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java

@@ -1344,7 +1344,7 @@ public void setProofFile(File proofFile) {
     }
 
     public void saveToFile(File file) throws IOException {
-        ProofSaver saver = new ProofSaver(this, file);
+        ProofSaver saver = new ProofSaver(this, null, file);
         saver.save();
     }
 
@@ -1356,7 +1356,7 @@ public void saveToFile(File file) throws IOException {
      * @throws IOException on any I/O error
      */
     public void saveProofObligationToFile(File file) throws IOException {
-        ProofSaver saver = new ProofSaver(this, file, false);
+        ProofSaver saver = new ProofSaver(this, null, file, false);
         saver.save();
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java

@@ -742,15 +742,18 @@ private ReplayResult replayProof(Proof proof) {
             replayResult =
                 replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon());
 
-            lastTouchedNode = replayResult.getLastSelectedGoal() != null
-                    ? replayResult.getLastSelectedGoal().node()
-                    : proof.root();
+            lastTouchedNode =
+                    replayResult.savedSelectedNode() != null ?
+                            replayResult.savedSelectedNode() :
+                        replayResult.lastSelectedGoal() != null
+                        ? replayResult.lastSelectedGoal().node()
+                        : proof.root();
 
         } catch (Exception e) {
             if (parserResult == null || parserResult.errors() == null
                     || parserResult.errors().isEmpty() || replayer == null
-                    || replayResult == null || replayResult.getErrors() == null
-                    || replayResult.getErrors().isEmpty()) {
+                    || replayResult == null || replayResult.errors() == null
+                    || replayResult.errors().isEmpty()) {
                 // this exception was something unexpected
                 errors.add(e);
             }
@@ -760,10 +763,10 @@ private ReplayResult replayProof(Proof proof) {
                 errors.addAll(parserResult.errors());
             }
             status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n")
-                    + (replayResult != null ? replayResult.getStatus()
+                    + (replayResult != null ? replayResult.status()
                             : "Error while loading proof.");
             if (replayResult != null) {
-                errors.addAll(replayResult.getErrors());
+                errors.addAll(replayResult.errors());
             }
 
             StrategyProperties newProps =

key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java

@@ -146,7 +146,7 @@ private void save(final String filename, final Proof proof) {
         // there may be concurrent changes to the proof... whatever
         final Runnable r = () -> {
             try {
-                new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save();
+                new ProofSaver(proof, null, filename, KeYConstants.INTERNAL_VERSION).save();
                 LOGGER.info("File saved: {}", filename);
             } catch (Exception e) {
                 LOGGER.error("Autosaving file  {} failed.", filename, e);

key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java

@@ -8,6 +8,7 @@
 import java.io.IOException;
 import java.util.zip.GZIPOutputStream;
 
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 
 /**
@@ -22,11 +23,12 @@ public class GZipProofSaver extends ProofSaver {
      * Instantiates a new proof saver.
      *
      * @param proof the non-<code>null</code> proof to save
+     * @param selectedNode the Node selected at time of saving or <code>null</code> if no information available
      * @param fileName the name of the file to write to
      * @param internalVersion the internal version
      */
-    public GZipProofSaver(Proof proof, String fileName, String internalVersion) {
-        super(proof, fileName, internalVersion);
+    public GZipProofSaver(Proof proof, Node selectedNode, String fileName, String internalVersion) {
+        super(proof, selectedNode, fileName, internalVersion);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java

@@ -33,7 +33,7 @@ enum ProofElementID {
         USER_INTERACTION("userinteraction"), PROOF_SCRIPT("proofscript"), NEW_NAMES("newnames"),
         AUTOMODE_TIME("autoModeTime"), KeY_LOG("keyLog"), KeY_USER("keyUser"),
         KeY_VERSION("keyVersion"), KeY_SETTINGS("keySettings"), OPEN_GOAL("opengoal"),
-        NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality");
+        NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"), SELECTED_NODE("selected");
 
         private final String rawName;
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java

@@ -72,6 +72,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser
     private BranchNodeIntermediate root = null; // the "dummy ID" branch
     private NodeIntermediate currNode;
     private final LinkedList<Throwable> errors = new LinkedList<>();
+    private boolean parsingOpenGoal = false;
 
     /**
      * @param proof Proof object for storing meta information about the parsed proof.
@@ -218,6 +219,9 @@ public void beginExpr(ProofElementID eid, String str) {
             }
         }
         case SOLVERTYPE -> ((BuiltinRuleInformation) ruleInfo).solver = str;
+        case OPEN_GOAL -> {
+            parsingOpenGoal = true;
+        }
         default -> {
         }
         }
@@ -233,6 +237,24 @@ public void endExpr(ProofElementID eid, int lineNr) {
                 ((AppNodeIntermediate) currNode).setInteractiveRuleApplication(true);
             }
         }
+        case SELECTED_NODE -> {
+            int openGoalChildSelected = -1;
+            if (parsingOpenGoal) {
+                if (currNode instanceof BranchNodeIntermediate branchNode) {
+                    if (!stack.isEmpty()) {
+                        if (stack.peek() instanceof AppNodeIntermediate parentAppNode) {
+                            openGoalChildSelected = parentAppNode.getChildren().size() - 1;
+                            parentAppNode.setSelectedNode(true, openGoalChildSelected);
+                        }
+                    }
+                } else {
+                    openGoalChildSelected = 0;
+                }
+            }
+            if (currNode != null && currNode instanceof AppNodeIntermediate appNode) {
+                appNode.setSelectedNode(true, openGoalChildSelected);
+            }
+        }
         case PROOF_SCRIPT -> {
             if (currNode != null) {
                 ((AppNodeIntermediate) currNode).setScriptRuleApplication(true);
@@ -252,6 +274,9 @@ public void endExpr(ProofElementID eid, int lineNr) {
                 builtinInfo.builtinIfInsts.append(new Pair<>(
                     builtinInfo.currIfInstFormula, builtinInfo.currIfInstPosInTerm));
         }
+        case OPEN_GOAL -> {
+           parsingOpenGoal = false;
+        }
         default -> {
         }
         }

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java

@@ -116,12 +116,15 @@ public class IntermediateProofReplayer {
     /** The current open goal */
     private Goal currGoal = null;
 
+    /** the node selected at time of saving, or null if information is not available */
+    private Node savedSelectedNode = null;
+
     /**
      * Constructs a new {@link IntermediateProofReplayer}.
      *
      * @param loader The problem loader, for reporting errors.
      * @param proof The proof object into which to load the replayed proof.
-     * @param intermediate
+     * @param parserResult result of the intermediate parser to be replayed
      */
     public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof,
             IntermediatePresentationProofFileParser.Result parserResult) {
@@ -223,6 +226,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
                     proof.getServices().getNameRecorder()
                             .setProposals(currInterm.getIntermediateRuleApp().getNewNames());
 
+
                     if (currInterm.getIntermediateRuleApp() instanceof TacletAppIntermediate) {
                         TacletAppIntermediate appInterm =
                             (TacletAppIntermediate) currInterm.getIntermediateRuleApp();
@@ -255,8 +259,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
                                 + appInterm.getRuleName() + NOT_APPLICABLE, e);
                         }
 
-                    } else if (currInterm
-                            .getIntermediateRuleApp() instanceof BuiltInAppIntermediate) {
+                    } else if (currInterm.getIntermediateRuleApp() instanceof BuiltInAppIntermediate) {
                         BuiltInAppIntermediate appInterm =
                             (BuiltInAppIntermediate) currInterm.getIntermediateRuleApp();
 
@@ -358,6 +361,18 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
                             }
                         }
                     }
+                    // set information if this node was the last selected node at the time of saving the
+                    // proof
+                    if (currInterm.getSelectedNode()) {
+                        // check whether the node itself was selected or a child that is an open goal
+                        int openChildSelected = currInterm.getOpenChildSelected();
+                        if (openChildSelected < 0 || openChildSelected >= currNode.childrenCount()) {
+                            savedSelectedNode = currNode;
+                        } else {
+                            savedSelectedNode = currNode.child(openChildSelected);
+                        }
+                    }
+
                 }
             } catch (Throwable throwable) {
                 // Default exception catcher -- proof should not stop loading
@@ -374,7 +389,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
             progressMonitor.setProgress(max);
         }
         LOGGER.debug("Proof replay took " + PerfScope.formatTime(System.nanoTime() - time));
-        return new Result(status, errors, currGoal);
+        return new Result(status, errors, currGoal, savedSelectedNode);
     }
 
     /**
@@ -1057,27 +1072,5 @@ static class SkipSMTRuleException extends Exception {
      *
      * @author Dominic Scheurer
      */
-    public static class Result {
-        private final String status;
-        private final List<Throwable> errors;
-        private Goal lastSelectedGoal = null;
-
-        public Result(String status, List<Throwable> errors, Goal lastSelectedGoal) {
-            this.status = status;
-            this.errors = errors;
-            this.lastSelectedGoal = lastSelectedGoal;
-        }
-
-        public String getStatus() {
-            return status;
-        }
-
-        public List<Throwable> getErrors() {
-            return errors;
-        }
-
-        public Goal getLastSelectedGoal() {
-            return lastSelectedGoal;
-        }
-    }
+    public record Result(String status, List<Throwable> errors, Goal lastSelectedGoal, Node savedSelectedNode) {}
 }

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -74,6 +74,10 @@ public class OutputStreamProofSaver {
      */
     protected final boolean saveProofSteps;
 
+    /**
+     * The currently selected node if available, otherwise null
+     */
+    protected final Node selectedNodeNr;
 
     /**
      * Extracts java source directory from {@link Proof#header()}, if it exists.
@@ -95,27 +99,27 @@ public static File getJavaSourceLocation(Proof proof) {
         return null;
     }
 
-    public OutputStreamProofSaver(Proof proof) {
-        this(proof, KeYConstants.INTERNAL_VERSION);
+    public OutputStreamProofSaver(Proof proof, Node selectedNode) {
+        this(proof, selectedNode, KeYConstants.INTERNAL_VERSION);
     }
 
-    public OutputStreamProofSaver(Proof proof, String internalVersion) {
-        this.proof = proof;
-        this.internalVersion = internalVersion;
-        this.saveProofSteps = true;
+    public OutputStreamProofSaver(Proof proof, Node selectedNode, String internalVersion) {
+        this(proof, selectedNode, internalVersion, true);
     }
 
     /**
      * Create a new OutputStreamProofSaver.
      *
      * @param proof the proof to save
+     * @param selectedNode the Node selected at time of saving or null if no information available
      * @param internalVersion currently running KeY version
      * @param saveProofSteps whether to save the performed proof steps
      */
-    public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) {
+    public OutputStreamProofSaver(Proof proof, Node selectedNode, String internalVersion, boolean saveProofSteps) {
         this.proof = proof;
         this.internalVersion = internalVersion;
         this.saveProofSteps = saveProofSteps;
+        this.selectedNodeNr = selectedNode;
     }
 
     /**
@@ -589,7 +593,11 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws
 
             printer.printSequent(node.sequent());
             output.append(escapeCharacters(printer.result().replace('\n', ' ')));
-            output.append("\")\n");
+            output.append("\"");
+            if (node == selectedNodeNr) {
+                output.append(" (" + ProofElementID.SELECTED_NODE.getRawName() + ")");
+            }
+            output.append(")\n");
             return;
         }
 
@@ -653,10 +661,13 @@ private void collectProof(Node node, String prefix, Appendable output) throws IO
      */
     private void userInteraction2Proof(Node node, Appendable output) throws IOException {
         if (node.getNodeInfo().getInteractiveRuleApplication()) {
-            output.append(" (userinteraction)");
+            output.append(" ("+ ProofElementID.USER_INTERACTION.getRawName() + ")");
+        }
+        if (node == selectedNodeNr) {
+            output.append(" (" + ProofElementID.SELECTED_NODE.getRawName() + ")");
         }
         if (node.getNodeInfo().getScriptRuleApplication()) {
-            output.append(" (proofscript)");
+            output.append(" (" + ProofElementID.PROOF_SCRIPT.getRawName() + ")");
         }
     }
 
@@ -716,7 +727,7 @@ public static String posInTerm2Proof(PosInTerm pos) {
     /**
      * Get the "interesting" instantiations of the provided object.
      *
-     * @see SVInstantiations#interesting
+     * @see SVInstantiations#interesting()
      * @param inst instantiations
      * @return the "interesting" instantiations (serialized)
      */

key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java

@@ -7,6 +7,7 @@
 import java.io.IOException;
 import java.nio.file.Paths;
 
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.io.consistency.AbstractFileRepo;
 import de.uka.ilkd.key.proof.io.consistency.FileRepo;
@@ -30,10 +31,11 @@ public class ProofBundleSaver extends ProofSaver {
      * Creates a new ProofBundleSaver.
      *
      * @param proof the proof to save
+     * @param selectedNode the Node selected at time of saving or null if no information available
      * @param saveFile the target filename
      */
-    public ProofBundleSaver(Proof proof, File saveFile) {
-        super(proof, saveFile);
+    public ProofBundleSaver(Proof proof, Node selectedNode, File saveFile) {
+        super(proof, selectedNode, saveFile);
     }
 
     @Override