Pruning a closed proof (and reopening it) did not update the proof st…

…atus in the task tree and also did not select any node/goal.
KeYProject · Nov 10, 2023 · 4f5a25b · 4f5a25b
1 parent 93cf0b0
commit 4f5a25b
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 11 deletions.
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
@@ -265,12 +265,16 @@ protected boolean filter(Taclet taclet) {
     public void setBack(Node node) {
         getUI().getProofControl().pruneTo(node);
         finishSetBack(node.proof());
+        keySelectionModel.setSelectedNode(node);
     }
 
     public void setBack(Goal goal) {
         if (getSelectedProof() != null) {
             getUI().getProofControl().pruneTo(goal);
-            finishSetBack(goal.proof());
+            final Proof proof = goal.proof();
+            finishSetBack(proof);
+            Node node = goal.node() == proof.root() ? goal.node() : goal.node().parent();
+            keySelectionModel.setSelectedNode(node);
         }
     }
 

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java
@@ -24,7 +24,6 @@
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.notification.events.AbandonTaskEvent;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.proof.ProofTreeAdapter;
 import de.uka.ilkd.key.proof.ProofTreeEvent;
 import de.uka.ilkd.key.proof.ProofTreeListener;
 import de.uka.ilkd.key.proof.mgt.BasicTask;
@@ -285,7 +284,7 @@ private void checkPopup(MouseEvent e) {
     /**
      * a prooftree listener, so that it is known when the proof has closed
      */
-    class TaskTreeProofTreeListener extends ProofTreeAdapter {
+    class TaskTreeProofTreeListener implements ProofTreeListener {
 
         /**
          * invoked if all goals of the proof are closed
@@ -295,17 +294,19 @@ public void proofClosed(ProofTreeEvent e) {
         }
 
         /**
-         * invoked if the list of goals changed (goals were added, removed etc.
+         * invoked if a proof has been pruned, potentially reopening branches
          */
-        public void proofGoalRemoved(ProofTreeEvent e) {
-        }
-
-        /** invoked if the current goal of the proof changed */
-        public void proofGoalsAdded(ProofTreeEvent e) {
+        public void proofPruned(ProofTreeEvent e) {
+            delegateView.repaint();
         }
 
-        /** invoked if the current goal of the proof changed */
-        public void proofGoalsChanged(ProofTreeEvent e) {
+        /**
+         * The structure of the proof has changed radically. Any client should rescan the whole
+         * proof
+         * tree.
+         */
+        public void proofStructureChanged(ProofTreeEvent e) {
+            delegateView.repaint();
         }
     } // end of prooftreelistener