Fix (for issue #3347) that node selection gets forgotten when switchi…

…ng between proofs (#3349)

key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java

@@ -112,7 +112,7 @@ public KeYMediator(AbstractMediatorUserInterfaceControl ui) {
         notationInfo = new NotationInfo();
         proofListener = new KeYMediatorProofListener();
         proofTreeListener = new KeYMediatorProofTreeListener();
-        keySelectionModel = new KeYSelectionModel(new KeYMediatorSelectionListener());
+        keySelectionModel = new KeYSelectionModel(this);
 
         ui.getProofControl().addAutoModeListener(proofListener);
 
@@ -214,11 +214,15 @@ public String toString() {
 
     /**
      * Selects the specified proof and initializes it.
+     * <br/>
+     * This method is called by the selection model, which fires the event.
+     * The method itself does not fire
+     * {@link KeYSelectionListener#selectedProofChanged(KeYSelectionEvent)}
      *
      * @param newProof the proof to select.
      * @param previousProof the previously selected proof
      */
-    private void setProof(Proof newProof, Proof previousProof) {
+    void setProof(Proof newProof, Proof previousProof) {
         if (previousProof == newProof) {
             return;
         }
@@ -239,8 +243,6 @@ private void setProof(Proof newProof, Proof previousProof) {
         }
 
         OneStepSimplifier.refreshOSS(newProof);
-
-        keySelectionModel.setSelectedProof(newProof);
     }
 
     /**
@@ -672,23 +674,7 @@ public void proofGoalsAdded(ProofTreeEvent e) {
         }
 
         @Override
-        public void proofStructureChanged(ProofTreeEvent e) {
-            if (isInAutoMode() || pruningInProcess) {
-                return;
-            }
-            Proof p = e.getSource();
-            if (p == getSelectedProof()) {
-                Node sel_node = getSelectedNode();
-                if (!p.find(sel_node)) {
-                    keySelectionModel.defaultSelection();
-                } else {
-                    // %%% hack does need to be done proper
-                    // needed top update that the selected node nay have
-                    // changed its status
-                    keySelectionModel.setSelectedNode(sel_node);
-                }
-            }
-        }
+        public void proofStructureChanged(ProofTreeEvent e) {}
     }
 
     private final class KeYMediatorProofListener implements RuleAppListener, AutoModeListener {
@@ -720,22 +706,6 @@ public void autoModeStopped(ProofEvent e) {
         }
     }
 
-    private class KeYMediatorSelectionListener implements KeYSelectionListener {
-        /** focused node has changed */
-        @Override
-        public void selectedNodeChanged(KeYSelectionEvent<Node> e) {
-            // empty
-        }
-
-        /**
-         * the selected proof has changed (e.g. a new proof has been loaded)
-         */
-        @Override
-        public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
-            setProof(e.getSource().getSelectedProof(), e.getPreviousSelection());
-        }
-    }
-
     /*
      * Disable certain actions until a proof is loaded.
      */

key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java

@@ -17,12 +17,8 @@
 public class KeYSelectionModel {
     private static final Logger LOGGER = LoggerFactory.getLogger(KeYSelectionModel.class);
 
-    // the listener to be informed before all
-    // this is the KeYMediator listener and should be removed later
-    // at the moment it is used to ensure a sane state of the mediator
-    // before other selection listeners receive change information
-    // TODO: remove usage of primary
-    private final KeYSelectionListener primary;
+    // the KeYMediator is informed before all
+    private final KeYMediator primary;
 
     /** the proof to listen to */
     private Proof proof;
@@ -47,7 +43,7 @@ public class KeYSelectionModel {
 
     /** cached selected node event */
 
-    public KeYSelectionModel(KeYSelectionListener primary) {
+    public KeYSelectionModel(KeYMediator primary) {
         this.primary = primary;
         listenerList = Collections.synchronizedList(new ArrayList<>(5));
         goalIsValid = false;
@@ -83,6 +79,7 @@ public synchronized void setSelectedProof(Proof p) {
         final Proof previousProof = proof;
         goalIsValid = false;
         proof = p;
+        primary.setProof(p, previousProof);
         if (proof != null) {
             Goal g = proof.openGoals().iterator().next();
             if (g == null) {
@@ -102,6 +99,8 @@ public synchronized void setSelectedProof(Proof p) {
             selectedRuleApp = null;
             selectedGoal = null;
         }
+
+
         fireSelectedProofChanged(previousProof);
     }
 
@@ -309,8 +308,8 @@ public void defaultSelection() {
 
     /**
      * selects the first open goal below the given node <tt>old</tt> if no open goal is available
-     * node <tt>old</tt> is selected. In case that <tt>old</tt> has been removed from the proof the
-     * proof root is selected
+     * node <tt>old</tt> is selected. In case that <tt>old</tt> has been removed from the proof, the
+     * proof root is selected.
      *
      * @param old the Node to start looking for open goals
      */
@@ -381,7 +380,6 @@ public synchronized void fireSelectedNodeChanged(Node previousNode) {
         synchronized (listenerList) {
             final KeYSelectionEvent<Node> selectionEvent =
                 new KeYSelectionEvent<>(this, previousNode);
-            primary.selectedNodeChanged(selectionEvent);
             for (final KeYSelectionListener listener : listenerList) {
                 listener.selectedNodeChanged(selectionEvent);
             }
@@ -393,7 +391,6 @@ public synchronized void fireSelectedProofChanged(Proof previousProof) {
             LOGGER.debug("Selected Proof changed, firing...");
             final KeYSelectionEvent<Proof> selectionEvent =
                 new KeYSelectionEvent<>(this, previousProof);
-            primary.selectedProofChanged(selectionEvent);
             for (final KeYSelectionListener listener : listenerList) {
                 listener.selectedProofChanged(selectionEvent);
             }

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -1163,7 +1163,6 @@ public void addProblem(final de.uka.ilkd.key.proof.ProofAggregate plist) {
             addToProofList(plist);
             getMediator().getSelectionModel().setSelectedProof(plist.getFirstProof());
             disableCurrentGoalView = false;
-            updateSequentView();
         };
         ThreadUtilities.invokeOnEventQueue(guiUpdater);
     }
@@ -1172,11 +1171,9 @@ public void addProblem(final de.uka.ilkd.key.proof.ProofAggregate plist) {
      * Updates the sequent displayed in the main frame.
      */
     private synchronized void updateSequentView() {
-
         if (disableCurrentGoalView) {
             return;
         }
-
         final SequentView newSequentView;
 
         // if this is set we can skip calls to printSequent, since it is invoked in setSequentView
@@ -1656,7 +1653,6 @@ private void setToolBarEnabled() {
 
         @Override
         public void modalDialogOpened(EventObject e) {
-
             if (e.getSource() instanceof ApplyTacletDialog) {
                 // disable all elements except the sequent window (drag'n'drop !) ...
                 enableMenuBar(MainWindow.this.getJMenuBar(), false);

key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java

@@ -12,6 +12,8 @@
 import java.util.LinkedList;
 import java.util.List;
 import javax.swing.*;
+import javax.swing.event.TreeSelectionEvent;
+import javax.swing.event.TreeSelectionListener;
 import javax.swing.tree.DefaultTreeCellRenderer;
 import javax.swing.tree.TreePath;
 
@@ -58,6 +60,21 @@ public class TaskTree extends JPanel {
     /** listener to the prof tree events */
     private final ProofTreeListener proofTreeListener = new TaskTreeProofTreeListener();
 
+    private final TreeSelectionListener selectionListener = new TreeSelectionListener() {
+        /**
+         * listen to changes in the delegateView {@link JTree} selections and initiate switch
+         * between proofs if necessary
+         *
+         * @param e the event that characterizes the change.
+         */
+        @Override
+        public void valueChanged(TreeSelectionEvent e) {
+            if (e.getSource() == delegateView) {
+                problemChosen();
+            }
+        }
+    };
+
     /** the list model to be used */
     private final TaskTreeModel model = new TaskTreeModel();
 
@@ -87,6 +104,7 @@ public void autoModeStarted(ProofEvent e) {
         delegateView.setModel(model);
         delegateView.setCellRenderer(new TaskTreeIconCellRenderer());
         delegateView.addMouseListener(mouseListener);
+        delegateView.addTreeSelectionListener(selectionListener);
         this.setLayout(new BorderLayout());
         this.add(delegateView, BorderLayout.CENTER);
         delegateView.setShowsRootHandles(false);
@@ -175,7 +193,8 @@ public BasicTask[] getAllSelectedBasicTasks() {
     /** called when the user has clicked on a problem */
     private void problemChosen() {
         TaskTreeNode prob = getSelectedTask();
-        if (prob != null && prob.proof() != null && mediator != null) {
+        if (prob != null && prob.proof() != null && mediator != null &&
+                mediator.getSelectedProof() != prob.proof()) {
             mediator.getSelectionModel().setSelectedProof(prob.proof());
         }
     }
@@ -255,7 +274,6 @@ class TaskTreeMouseListener extends MouseAdapter {
 
         @Override
         public void mouseClicked(MouseEvent e) {
-            problemChosen();
             checkPopup(e);
         }
 
@@ -284,13 +302,11 @@ private void checkPopup(MouseEvent e) {
                 TreePath selPath = delegateView.getPathForLocation(e.getX(), e.getY());
                 if (selPath != null && selPath.getLastPathComponent() instanceof BasicTask task) {
                     Proof p = task.proof();
-                    mediator.getSelectionModel().setSelectedProof(p);
+                    delegateView.setSelectionPath(selPath);
                     JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu(
-                        DefaultContextMenuKind.PROOF_LIST, mediator.getSelectedProof(), mediator);
+                        DefaultContextMenuKind.PROOF_LIST, p, mediator);
                     menu.show(e.getComponent(), e.getX(), e.getY());
                 }
-            } else {
-                problemChosen();
             }
         }
     }

key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java

@@ -167,7 +167,6 @@ protected SequentView(MainWindow mainWindow) {
         addPropertyChangeListener("font", changeListener);
         addHierarchyBoundsListener(changeListener);
 
-
         // Register tooltip
         setToolTipText("");
 

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java

@@ -518,8 +518,12 @@ private void setProof(Proof p) {
                 delegateView.setSelectionPath(delegateModel.getSelection());
                 delegateView.scrollPathToVisible(delegateModel.getSelection());
             } else {
-                // new proof, select initial node
-                delegateView.setSelectionRow(1);
+                if (mediator.getSelectedProof() == p && mediator.getSelectedNode() != null) {
+                    makeNodeVisible(mediator.getSelectedNode());
+                } else {
+                    // new proof with not yet selected node, select initial node
+                    delegateView.setSelectionRow(1);
+                }
             }
 
             // Restore previous scroll position.