diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index 0d3fd45622c..80d4b90337e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java @@ -253,8 +253,8 @@ public void applyInteractive(RuleApp app, Goal goal) { /** * Prunes a proof to the given node. * - * @param node - * @see {@link Proof#pruneProof(Node)} + * @param node the node to prune to + * @see Proof#pruneProof(Node) */ public void pruneTo(Node node) { node.proof().pruneProof(node); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java index 03f8f392add..13c7a0be3fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java @@ -7,6 +7,7 @@ import javax.swing.*; import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.MergePartner; import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp; @@ -37,6 +38,15 @@ class ProofPruner { */ public ImmutableList prune(final Node cuttingPoint) { + // very special case: prune of cached branch + // (simply reopen the cached branch) + var closedBy = cuttingPoint.lookup(ClosedBy.class); + if (closedBy != null) { + cuttingPoint.deregister(closedBy, ClosedBy.class); + cuttingPoint.proof().reOpenGoal(cuttingPoint.proof().getClosedGoal(cuttingPoint)); + return ImmutableList.of(cuttingPoint); + } + // there is only one leaf containing an open goal that is interesting for pruning the // subtree of node, namely the first leave that is found by a breadth // first search. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java index 3866cf218af..6f8da873e7a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java @@ -32,6 +32,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.delayedcut.DelayedCutListener; import de.uka.ilkd.key.proof.delayedcut.DelayedCutProcessor; +import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; @@ -400,6 +401,9 @@ public Prune(ProofTreeContext context) { .getClosedSubtreeGoals(context.invokedNode).size() > 0))) { setEnabled(true); } + if (context.invokedNode.lookup(ClosedBy.class) != null) { + setEnabled(true); + } } }