fix errors from rebasing

Author: wadoon

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

@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.proof.io.SingleThreadProblemLoader;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
+import de.uka.ilkd.key.settings.Configuration;
 
 import org.key_project.prover.engine.ProverCore;
 import org.key_project.prover.engine.ProverTaskListener;

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

@@ -185,6 +185,17 @@ public String getProblemHeader() {
             }
             return "";
         }
+
+        /// Returns the raw settings within a [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 static class ConfigurationFile extends KeyAst<KeYParser.CfileContext> {

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

@@ -11,7 +11,6 @@
 import de.uka.ilkd.key.proof.reference.ClosedBy;
 import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.merge.MergeRule;
-import de.uka.ilkd.key.util.Pair;
 
 import org.key_project.logic.op.Function;
 import org.key_project.prover.rules.RuleApp;

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

@@ -60,6 +60,8 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.KeYCollections;
 
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 

key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java

@@ -268,7 +268,7 @@ public List<Object> getList(String name) {
 
     /**
      * Returns a list of strings for the given name.
-     *
+     * <p>
      * In contrast to the other methods, this method does not throw an exception if the entry does
      * not
      * exist in the configuration. Instead, it returns an empty list.
@@ -433,14 +433,19 @@ public void overwriteWith(Configuration other) {
     }
 
     // TODO Add documentation for this.
+
     /**
      * POJO for metadata of configuration entries.
      */
     public static class ConfigurationMeta {
-        /** Position of declaration within a file */
+        /**
+         * Position of declaration within a file
+         */
         private Position position;
 
-        /** documentation given in the file */
+        /**
+         * documentation given in the file
+         */
         private String documentation;
 
         public Position getPosition() {
@@ -550,6 +555,19 @@ private ConfigurationWriter print(String s) {
             return this;
         }
 
+        private ConfigurationWriter printSeq(int[] values) {
+            out.format("[");
+            for (var i = 0; i < values.length; i++) {
+                int o = values[i];
+                printValue(o);
+                if (i + 1 < values.length) {
+                    print(", ");
+                }
+            }
+            out.format("]");
+            return this;
+        }
+
         private ConfigurationWriter printSeq(Collection<?> value) {
             out.format("[ ");
             indent += 4;

key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java

@@ -34,6 +34,7 @@
 import de.uka.ilkd.key.proof.io.*;
 import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
+import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.settings.ViewSettings;
@@ -509,8 +510,10 @@ public void loadingStarted(AbstractProblemLoader loader) {
 
     @Override
     public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer,
-            ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException {
-        super.loadingFinished(loader, poContainer, proofList, result);
+            ProofAggregate proofList, ReplayResult result, Configuration settings)
+            throws ProblemLoaderException {
+
+        super.loadingFinished(loader, poContainer, proofList, result, settings);
         if (proofList != null) {
             if (result != null) {
                 if ("".equals(result.getStatus())) {
@@ -532,22 +535,21 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo
         if (poContainer != null
                 && poContainer.getProofOblInput() instanceof KeYUserProblemFile file) {
             // TODO weigl not triggered
-            var settings = file.readSettings();
             var addInfo = settings.getSection(ProofSettings.KEY_ADDITIONAL_DATA);
             if (addInfo != null) {
                 var lastSelectedNodePath =
                     settings.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE);
                 if (lastSelectedNodePath != null && proofList != null) {
                     var proof = proofList.getFirstProof();
-                    proof.root().traversePath(lastSelectedNodePath.iterator());
+                    var selectedNode = proof.root().traversePath(
+                        lastSelectedNodePath.stream().map(Long::intValue).iterator());
+                    getMediator().getSelectionModel().setSelectedNode(selectedNode);
                 }
             }
             file.close();
         }
     }
 
-
-
     /**
      * Loads the given location and returns all required references as {@link KeYEnvironment} with
      * KeY's {@link MainWindow}.