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

key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java

@@ -26,6 +26,7 @@
 import de.uka.ilkd.key.prover.ProverTaskListener;
 import de.uka.ilkd.key.prover.TaskFinishedInfo;
 import de.uka.ilkd.key.prover.TaskStartedInfo;
+import de.uka.ilkd.key.settings.Configuration;
 
 import org.slf4j.LoggerFactory;
 
@@ -255,7 +256,8 @@ public void loadingStarted(AbstractProblemLoader loader) {
 
     @Override
     public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer,
-            ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException {
+            ProofAggregate proofList, ReplayResult result, Configuration settings)
+            throws ProblemLoaderException {
         if (proofList != null) {
             // avoid double registration at spec repos as that is done already earlier in
             // createProof

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -10,7 +10,7 @@
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.parser.Location;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
@@ -20,7 +20,6 @@
 import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
-import de.uka.ilkd.key.util.Pair;
 
 /**
  * Instances of this class are used to collect and access all relevant information for verification
@@ -47,7 +46,7 @@ public class KeYEnvironment<U extends UserInterfaceControl> {
     /**
      * An optional field denoting a script contained in the proof file.
      */
-    private final Pair<String, Location> proofScript;
+    private final KeyAst.ProofScriptEntry proofScript;
 
     /**
      * Indicates that this {@link KeYEnvironment} is disposed.
@@ -76,7 +75,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) {
      * @param initConfig The loaded project.
      */
     public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof,
-            Pair<String, Location> proofScript, ReplayResult replayResult) {
+            KeyAst.ProofScriptEntry proofScript, ReplayResult replayResult) {
         this.ui = ui;
         this.initConfig = initConfig;
         this.loadedProof = loadedProof;
@@ -316,7 +315,7 @@ public boolean isDisposed() {
         return disposed;
     }
 
-    public Pair<String, Location> getProofScript() {
+    public KeyAst.ProofScriptEntry getProofScript() {
         return proofScript;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java

@@ -14,6 +14,7 @@
 
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.java.Position;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -67,6 +68,10 @@ public ProofScriptEngine(String script, Location initLocation, Goal initiallySel
         this.initiallySelectedGoal = initiallySelectedGoal;
     }
 
+    public ProofScriptEngine(KeyAst.ProofScriptEntry script) {
+        this(script.code(), script.getLocation());
+    }
+
     private static Map<String, ProofScriptCommand<?>> loadCommands() {
         Map<String, ProofScriptCommand<?>> result = new HashMap<>();
         var loader = ServiceLoader.load(ProofScriptCommand.class);

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -3,17 +3,19 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser;
 
+import java.net.URI;
 import java.net.URL;
 import java.util.List;
 
+import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.nparser.builder.BuilderHelpers;
 import de.uka.ilkd.key.nparser.builder.ChoiceFinder;
 import de.uka.ilkd.key.nparser.builder.FindProblemInformation;
 import de.uka.ilkd.key.nparser.builder.IncludeFinder;
+import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.init.Includes;
 import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.settings.ProofSettings;
-import de.uka.ilkd.key.util.Triple;
 
 import org.key_project.util.java.StringUtil;
 
@@ -73,11 +75,28 @@ public static class File extends KeyAst<KeYParser.FileContext> {
             return settings;
         }
 
-        public @Nullable Triple<String, Integer, Integer> findProofScript() {
+        /**
+         * Returns the raw settings within a {@link de.uka.ilkd.key.proof.io.KeYFile}.
+         */
+        public Configuration findSettings() {
+            final var cfg = new ConfigurationBuilder();
+            if (ctx.preferences() == null || ctx.preferences().cvalue() == null) {
+                return new Configuration();
+            }
+
+            var c = ctx.preferences().cvalue();
+            return (Configuration) c.accept(cfg);
+        }
+
+
+        public @Nullable ProofScriptEntry findProofScript() {
             if (ctx.problem() != null && ctx.problem().proofScript() != null) {
                 KeYParser.ProofScriptContext pctx = ctx.problem().proofScript();
                 String text = pctx.ps.getText();
-                return new Triple<>(StringUtil.trim(text, '"'), pctx.ps.getLine(),
+                return new ProofScriptEntry(
+                    StringUtil.trim(text, '"'),
+                    URI.create(pctx.start.getInputStream().getSourceName()),
+                    pctx.ps.getLine(),
                     pctx.ps.getCharPositionInLine());
             }
             return null;
@@ -167,4 +186,17 @@ public Taclet(KeYParser.TacletContext taclet) {
             super(taclet);
         }
     }
+
+    /**
+     * This class represents the entry of a proof script within a KeY file.
+     *
+     * @param code               non-null string containing the proof script
+     * @param line               line number of the entry
+     * @param charPositionInLine starting offset position in the line
+     */
+    public record ProofScriptEntry(@NonNull String code, URI source, int line, int charPositionInLine) {
+        public Location getLocation() {
+            return new Location(source, Position.newOneBased(this.line(), this.charPositionInLine()));
+        }
+    }
 }

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

@@ -3,15 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.LinkedHashSet;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.ListIterator;
+import java.util.*;
 
 import de.uka.ilkd.key.logic.RenamingTable;
 import de.uka.ilkd.key.logic.Sequent;
@@ -49,10 +41,14 @@ public class Node implements Iterable<Node> {
 
     private static final String NODES = "nodes";
 
-    /** the proof the node belongs to */
+    /**
+     * the proof the node belongs to
+     */
     private final Proof proof;
 
-    /** The parent node. **/
+    /**
+     * The parent node.
+     **/
     private Node parent = null;
     /**
      * The branch location of this proof node.
@@ -81,7 +77,9 @@ public class Node implements Iterable<Node> {
 
     private boolean closed = false;
 
-    /** contains non-logical content, used for user feedback */
+    /**
+     * contains non-logical content, used for user feedback
+     */
     private NodeInfo nodeInfo;
 
     /**
@@ -162,7 +160,9 @@ public void setSequent(Sequent seq) {
         this.seq = seq;
     }
 
-    /** returns the sequent of this node */
+    /**
+     * returns the sequent of this node
+     */
     public Sequent sequent() {
         return seq;
     }
@@ -176,7 +176,9 @@ public NodeInfo getNodeInfo() {
         return nodeInfo;
     }
 
-    /** returns the proof the Node belongs to */
+    /**
+     * returns the proof the Node belongs to
+     */
     public Proof proof() {
         return proof;
     }
@@ -225,14 +227,16 @@ public RuleApp getAppliedRuleApp() {
         return appliedRuleApp;
     }
 
-    /** Returns the set of NoPosTacletApps at this node */
+    /**
+     * Returns the set of NoPosTacletApps at this node
+     */
     public Iterable<NoPosTacletApp> getLocalIntroducedRules() {
         return localIntroducedRules;
     }
 
     /**
      * Returns the set of created program variables known in this node.
-     *
+     * <p>
      * In the resulting list, the newest additions come first.
      *
      * @returns a non-null immutable list of program variables.
@@ -249,7 +253,7 @@ public void addLocalProgVars(Iterable<? extends IProgramVariable> elements) {
 
     /**
      * Returns the set of freshly created function symbols known to this node.
-     *
+     * <p>
      * In the resulting list, the newest additions come first.
      *
      * @return a non-null immutable list of function symbols.
@@ -471,13 +475,14 @@ public Iterator<Node> subtreeIterator() {
         return new SubtreeIterator(this);
     }
 
-    /** @return number of children */
+    /**
+     * @return number of children
+     */
     public int childrenCount() {
         return children.size();
     }
 
     /**
-     *
      * @param i an index (starting at 0).
      * @return the i-th child of this node.
      */
@@ -667,7 +672,9 @@ public boolean sanityCheckDoubleLinks() {
         return true;
     }
 
-    /** marks a node as closed */
+    /**
+     * marks a node as closed
+     */
     Node close() {
         closed = true;
         Node tmp = parent;
@@ -684,7 +691,7 @@ Node close() {
     /**
      * Opens a previously closed node and all its closed parents.
      * <p>
-     *
+     * <p>
      * This is, for instance, needed for the {@link MergeRule}: In a situation where a merge node
      * and its associated partners have been closed and the merge node is then pruned away, the
      * partners have to be reopened again. Otherwise, we have a soundness issue.
@@ -699,7 +706,9 @@ void reopen() {
         clearNameCache();
     }
 
-    /** @return true iff this inner node is closeable */
+    /**
+     * @return true iff this inner node is closeable
+     */
     private boolean isCloseable() {
         assert childrenCount() > 0;
         for (Node child : children) {
@@ -837,4 +846,37 @@ public int getStepIndex() {
     void setStepIndex(int stepIndex) {
         this.stepIndex = stepIndex;
     }
+
+    /**
+     * Calculates an array is the path from root node to this node. Each entry defines the child to
+     * be selected.
+     *
+     * @see #traversePath(Iterator)
+     */
+    public int[] getPosInProof() {
+        // collect the path from the current to node to the root of the proof.
+        // each entry is the children position
+        var path = new LinkedList<Integer>();
+        var current = this;
+        while (current.parent != null) {
+            path.add(0, current.parent.getChildNr(current));
+            current = current.parent;
+        }
+        return path.stream().mapToInt(it -> it).toArray();
+    }
+
+
+    /**
+     * Traverses a given iterator (child selection).
+     *
+     * @param traverse non-null
+     */
+    public Node traversePath(Iterator<Integer> traverse) {
+        var current = this;
+        while (traverse.hasNext()) {
+            int child = traverse.next();
+            current = current.child(child);
+        }
+        return current;
+    }
 }