Interactive Proof Replayer

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

@@ -143,16 +143,20 @@ public void beginExpr(ProofElementID eid, String str) {
                 tacletInfo.ifDirectFormulaList = tacletInfo.ifDirectFormulaList.append(str);
             }
             case KeY_USER -> { // UserLog
-                if (proof.userLog == null) {
-                    proof.userLog = new ArrayList<>();
+                if(proof != null) {
+                    if (proof.userLog == null) {
+                        proof.userLog = new ArrayList<>();
+                    }
+                    proof.userLog.add(str);
                 }
-                proof.userLog.add(str);
             }
             case KeY_VERSION -> { // Version log
-                if (proof.keyVersionLog == null) {
-                    proof.keyVersionLog = new ArrayList<>();
+                if(proof != null) {
+                    if (proof.keyVersionLog == null) {
+                        proof.keyVersionLog = new ArrayList<>();
+                    }
+                    proof.keyVersionLog.add(str);
                 }
-                proof.keyVersionLog.add(str);
             }
             case KeY_SETTINGS -> // ProofSettings
                 loadPreferences(str);

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

@@ -249,7 +249,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
                             .getIntermediateRuleApp() instanceof TacletAppIntermediate appInterm) {
 
                         try {
-                            currGoal.apply(constructTacletApp(appInterm, currGoal));
+                            currGoal.apply(constructTacletApp(proof, appInterm, currGoal));
 
                             final Iterator<Node> children = currNode.childrenIterator();
                             final LinkedList<NodeIntermediate> intermChildren =
@@ -439,12 +439,13 @@ public Collection<Throwable> getErrors() {
     /**
      * Constructs a taclet application from an intermediate one.
      *
+     * @param proof the current proof to operate on
      * @param currInterm The intermediate taclet application to create a "real" application for.
-     * @param currGoal The goal on which to apply the taclet app.
+     * @param currGoal   The goal on which to apply the taclet app.
      * @return The taclet application corresponding to the supplied intermediate representation.
      * @throws TacletAppConstructionException In case of an error during construction.
      */
-    private TacletApp constructTacletApp(TacletAppIntermediate currInterm, Goal currGoal)
+    public static TacletApp constructTacletApp(Proof proof, TacletAppIntermediate currInterm, Goal currGoal)
             throws TacletAppConstructionException {
 
         final String tacletName = currInterm.getRuleName();

key.ui/src/main/java/de/uka/ilkd/key/gui/proofreplay/ProofReapplicationExtension.java

@@ -0,0 +1,32 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.gui.proofreplay;
+
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+import de.uka.ilkd.key.gui.extension.api.TabPanel;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+import java.util.Collection;
+import java.util.List;
+
+@KeYGuiExtension.Info(name = "Proof Replayer", experimental = false, optional = true,
+        description = """
+                UI to help replaying stored proofs on new KeY versions. 
+                """
+)
+@NullMarked
+public class ProofReapplicationExtension implements KeYGuiExtension, KeYGuiExtension.LeftPanel {
+    private @Nullable ProofReapplicationView view;
+
+    @Override
+    public Collection<TabPanel> getPanels(MainWindow window, KeYMediator mediator) {
+        if (view == null) {
+            view = new ProofReapplicationView(window, mediator);
+        }
+        return List.of(view);
+    }
+}