Allow realizing multiple cached branches at once

keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java

@@ -4,6 +4,8 @@
 package de.uka.ilkd.key.gui.plugins.caching.actions;
 
 import java.awt.event.ActionEvent;
+import java.util.ArrayList;
+import java.util.List;
 
 import de.uka.ilkd.key.core.KeYMediator;
 import de.uka.ilkd.key.gui.IssueDialog;
@@ -30,37 +32,45 @@ public final class CopyReferencedProof extends KeyAction {
      */
     private final KeYMediator mediator;
     /**
-     * The node to copy the steps to.
+     * The nodes to copy the steps to.
      */
-    private final Node node;
+    private final List<Node> nodes;
 
     /**
      * Construct a new action.
      *
      * @param mediator the mediator
-     * @param node the node
+     * @param node the node to apply the action on
      */
     public CopyReferencedProof(KeYMediator mediator, Node node) {
         this.mediator = mediator;
-        this.node = node;
+        this.nodes = new ArrayList<>();
         setName("Copy referenced proof steps here");
-        setEnabled(node.leaf() && node.isClosed()
-                && node.lookup(ClosedBy.class) != null);
+        var iter = node.leavesIterator();
+        while (iter.hasNext()) {
+            var goal = iter.next();
+            if (goal.isClosed() && goal.lookup(ClosedBy.class) != null) {
+                nodes.add(goal);
+            }
+        }
+        setEnabled(!nodes.isEmpty());
         setMenuPath("Proof Caching");
     }
 
     @Override
     public void actionPerformed(ActionEvent e) {
-        ClosedBy c = node.lookup(ClosedBy.class);
-        Goal current = node.proof().getClosedGoal(node);
-        try {
-            mediator.stopInterface(true);
-            new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current,
-                c.nodesToSkip());
-            mediator.startInterface(true);
-        } catch (Exception ex) {
-            LOGGER.error("failed to copy proof ", ex);
-            IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex);
+        for (Node node : nodes) {
+            ClosedBy c = node.lookup(ClosedBy.class);
+            Goal current = node.proof().getClosedGoal(node);
+            try {
+                mediator.stopInterface(true);
+                new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current,
+                    c.nodesToSkip());
+                mediator.startInterface(true);
+            } catch (Exception ex) {
+                LOGGER.error("failed to copy proof ", ex);
+                IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex);
+            }
         }
     }
 }

keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java

@@ -19,12 +19,17 @@
 import org.key_project.slicing.DependencyTracker;
 import org.key_project.slicing.analysis.AnalysisResults;
 
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
 /**
  * Utility class for proof caching.
  *
  * @author Arne Keller
  */
 public final class ReferenceSearcher {
+    public static final Logger LOGGER = LoggerFactory.getLogger(ReferenceSearcher.class);
+
     private ReferenceSearcher() {
 
     }
@@ -91,8 +96,9 @@ public static ClosedBy findPreviousProof(List<Proof> previousProofs, Node newNod
                     .noneMatch(x -> x.node().lookup(ClosedBy.class) != null)) {
                 try {
                     results = depTracker.analyze(true, false);
-                } catch (Exception ignored) {
+                } catch (Exception e) {
                     // if the analysis for some reason fails, we simply proceed as usual
+                    LOGGER.debug("failed to analyze target proof ", e);
                 }
             }
             while (!nodesToCheck.isEmpty()) {