Skip to content

Commit 4448f7a

Browse files
Fix prune of cached proof branch
Closes #3846
1 parent c3ec3e4 commit 4448f7a

2 files changed

Lines changed: 12 additions & 1 deletion

File tree

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import javax.swing.*;
88

99
import de.uka.ilkd.key.proof.init.InitConfig;
10+
import de.uka.ilkd.key.proof.reference.ClosedBy;
1011
import de.uka.ilkd.key.rule.NoPosTacletApp;
1112
import de.uka.ilkd.key.rule.merge.MergePartner;
1213
import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp;
@@ -35,6 +36,16 @@ class ProofPruner {
3536
* @return the subtrees whose common root was the given {@code cuttingPoint}
3637
*/
3738
public ImmutableList<Node> prune(final Node cuttingPoint) {
39+
// special case: prune cached goal = only need to re-open the final node
40+
ClosedBy cby = cuttingPoint.lookup(ClosedBy.class);
41+
Goal goal = proof.getClosedGoal(cuttingPoint);
42+
if (cby != null && goal != null) {
43+
cuttingPoint.deregister(cby, ClosedBy.class);
44+
proof.reOpenGoal(goal);
45+
refreshGoal(goal, cuttingPoint);
46+
return ImmutableList.of(cuttingPoint);
47+
}
48+
3849
// there is only one leaf containing an open goal that is interesting for pruning the
3950
// subtree of <code>node</code>, namely the first leave that is found by a breadth
4051
// first search.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -146,7 +146,7 @@ public void ruleApplied(ProofEvent e) {
146146
if (!CachingSettingsProvider.getCachingSettings().getEnabled()) {
147147
return;
148148
}
149-
// new global off switch
149+
// new global off switch (toolbar)
150150
if (!getProofCachingEnabled()) {
151151
return;
152152
}

0 commit comments

Comments
 (0)