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

…ng between proofs

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);
     }
 
@@ -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);
             }