change in the listener delivers settings now

Author: wadoon

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

@@ -257,7 +257,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

@@ -12,6 +12,7 @@
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.nparser.KeyAst.ProofScript;

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

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
+import java.util.*;
+
 import de.uka.ilkd.key.logic.RenamingTable;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
 import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
@@ -15,16 +17,16 @@
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentChangeInfo;
 import de.uka.ilkd.key.util.Pair;
-import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.Nullable;
+
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.collection.Pair;
 import org.key_project.util.lookup.Lookup;
 
-import java.util.*;
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 
 public class Node implements Iterable<Node> {
     private static final String RULE_WITHOUT_NAME = "rule without name";
@@ -116,7 +118,7 @@ public class Node implements Iterable<Node> {
      * taclet with an addrule section on this node, then these taclets are stored in this list
      */
     private ImmutableSet<NoPosTacletApp> localIntroducedRules =
-            DefaultImmutableSet.nil();
+        DefaultImmutableSet.nil();
 
     /**
      * Holds the undo methods for the information added by rules to the {@code Goal.strategyInfos}.
@@ -448,7 +450,7 @@ List<Node> getLeaves() {
 
     /**
      * @return an iterator for the leaves of the subtree below this node. The computation is called
-     * at every call!
+     *         at every call!
      */
     public Iterator<Node> leavesIterator() {
         return new NodeIterator(getLeaves().iterator());
@@ -493,7 +495,7 @@ public Node child(int i) {
     /**
      * @param child a child of this node.
      * @return the number of the node <code>child</code>, if it is a child of this node (starting
-     * with <code>0</code>), <code>-1</code> otherwise
+     *         with <code>0</code>), <code>-1</code> otherwise
      */
     public int getChildNr(Node child) {
         int res = 0;
@@ -533,16 +535,16 @@ public StringBuffer getUniqueTacletId() {
      * Helper for {@link #toString()}
      *
      * @param prefix needed to keep track if a line has to be printed
-     * @param tree   the tree representation we want to add this subtree " @param preEnumeration the
-     *               enumeration of the parent without the last number
+     * @param tree the tree representation we want to add this subtree " @param preEnumeration the
+     *        enumeration of the parent without the last number
      * @param postNr the last number of the parents enumeration
-     * @param maxNr  the number of nodes at this level
-     * @param ownNr  the place of this node at this level
+     * @param maxNr the number of nodes at this level
+     * @param ownNr the place of this node at this level
      * @return the string representation of this node.
      */
 
     private StringBuffer toString(String prefix, StringBuffer tree, String preEnumeration,
-                                  int postNr, int maxNr, int ownNr) {
+            int postNr, int maxNr, int ownNr) {
         Iterator<Node> childrenIt = childrenIterator();
         // Some constants
         String frontIndent = (maxNr > 1 ? " " : "");
@@ -593,7 +595,7 @@ private StringBuffer toString(String prefix, StringBuffer tree, String preEnumer
         while (childrenIt.hasNext()) {
             childId++;
             childrenIt.next().toString(prefix, tree, newEnumeration, newPostNr, children.size(),
-                    childId);
+                childId);
         }
 
         return tree;
@@ -650,7 +652,7 @@ public String name() {
      * this node.
      *
      * @return true iff the parent of this node has this node as child and this condition holds also
-     * for the own children.
+     *         for the own children.
      */
     public boolean sanityCheckDoubleLinks() {
         if (!root()) {
@@ -777,7 +779,7 @@ public void addStrategyInfoUndoMethod(StrategyInfoUndoMethod undoMethod) {
     /**
      * Register a user-defined data in this node info.
      *
-     * @param obj     an object to be registered
+     * @param obj an object to be registered
      * @param service the key under it should be registered
      * @param <T> the type of the object to be registered
      */
@@ -788,9 +790,9 @@ public <T> void register(T obj, Class<T> service) {
     /**
      * Remove a previous registered user-defined data.
      *
-     * @param obj     registered object
+     * @param obj registered object
      * @param service the key under which the data was registered
-     * @param <T>     arbitray object
+     * @param <T> arbitray object
      */
     public <T> void deregister(T obj, Class<T> service) {
         if (userData != null) {
@@ -849,7 +851,8 @@ void setStepIndex(int stepIndex) {
     }
 
     /**
-     * Calculates an array is the path from root node to this node. Each entry defines the child to be selected.
+     * Calculates an array is the path from root node to this node. Each entry defines the child to
+     * be selected.
      *
      * @see #traversePath(Iterator)
      */

key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java

@@ -9,7 +9,6 @@
 
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.nparser.*;
-import de.uka.ilkd.key.nparser.builder.ProblemFinder;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofAggregate;
 import de.uka.ilkd.key.proof.io.IProofFileParser;
@@ -124,8 +123,8 @@ public ImmutableSet<PositionedString> read() throws ProofInputException {
         return warnings;
     }
 
-    public Configuration  readSettings() {
-        if(settings==null){
+    public Configuration readSettings() {
+        if (settings == null) {
             settings = getParseContext().findSettings();
         }
         return settings;
@@ -282,4 +281,5 @@ private Profile getDefaultProfile() {
     public KeYJavaType getContainerType() {
         return null;
     }
+
 }

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

@@ -279,7 +279,9 @@ public final void load(Consumer<Proof> callbackProofLoaded)
                 loadSelectedProof(poContainer, proofList, callbackProofLoaded);
             }
         } finally {
-            control.loadingFinished(this, poContainer, proofList, result);
+            var settings = (envInput instanceof KeYUserProblemFile kupf) ? kupf.readSettings()
+                    : new Configuration();
+            control.loadingFinished(this, poContainer, proofList, result, settings);
         }
     }
 
@@ -646,9 +648,6 @@ private ReplayResult replayProof(Proof proof) {
             problemInitializer.tryReadProof(parser, (KeYUserProblemFile) envInput);
             parserResult = parser.getResult();
 
-            // Parser is no longer needed, set it to null to free memory.
-            parser = null;
-
             // For loading, we generally turn on one step simplification to be
             // able to load proofs that used it even if the user has currently
             // turned OSS off.