From 4f5a25baadc97f437eea653738b8642d3a284f45 Mon Sep 17 00:00:00 2001
From: Richard Bubel <bubel@cs.tu-darmstadt.de>
Date: Thu, 9 Nov 2023 15:01:30 +0100
Subject: [PATCH] Pruning a closed proof (and reopening it) did not update the
 proof status in the task tree and also did not select any node/goal.

---
 .../de/uka/ilkd/key/core/KeYMediator.java     |  6 +++++-
 .../java/de/uka/ilkd/key/gui/TaskTree.java    | 21 ++++++++++---------
 2 files changed, 16 insertions(+), 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
index 3102b2ba53c..e2b7eb31f7c 100644
--- 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
index 100ff854d80..8a8ff4981b1 100644
--- 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