Make the proof tree (or the KeY GUI in general) responsive during automatic proof search

key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilter.java

@@ -82,6 +82,10 @@ public ImmutableList<SequentPrintFilterEntry> getFilteredSucc() {
      * entries.
      */
     protected void filterIdentity() {
+        if(originalSequent==null) {
+            return;
+        }
+
         antec = ImmutableSLList.nil();
         Iterator<SequentFormula> it = originalSequent.antecedent().iterator();
         while (it.hasNext()) {

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

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.control.ProofControl;
 import de.uka.ilkd.key.gui.GUIListener;
 import de.uka.ilkd.key.gui.UserActionListener;
+import de.uka.ilkd.key.gui.actions.MainWindowAction;
 import de.uka.ilkd.key.gui.actions.useractions.UserAction;
 import de.uka.ilkd.key.gui.notification.events.NotificationEvent;
 import de.uka.ilkd.key.gui.notification.events.ProofClosedNotificationEvent;
@@ -704,16 +705,22 @@ public void autoModeStopped(ProofEvent e) {
         }
     }
 
-    /*
-     * Disable certain actions until a proof is loaded.
-     */
+    /// Disable certain actions until a proof is loaded.
+    ///
+    /// ### DEPRECATION
+    /// You should rather use the [MainWindowAction] class
+    /// with the [MainWindowAction#updateEnablednessOnSelectionChange()] method.
+    ///
+    /// This provides more flexibility, as the enabledness can define in cases of a
+    /// combination of predicates.
+    ///
+    @Deprecated(forRemoval = true)
     public void enableWhenProofLoaded(final Action a) {
         a.setEnabled(getSelectedProof() != null);
         addKeYSelectionListener(new KeYSelectionListener() {
-
             @Override
             public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
-                a.setEnabled(e.getSource().getSelectedProof() != null);
+                a.setEnabled(e.source().getSelectedProof() != null);
             }
         });
     }
@@ -722,14 +729,14 @@ public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
      * Disable certain actions until a proof is loaded. This is a workaround for a broken proof
      * macro menu in the GUI. Remove this method as soon as another solution can be found.
      */
-    @Deprecated
+    @Deprecated(forRemoval = true)
     public void enableWhenProofLoaded(final javax.swing.AbstractButton a) {
         a.setEnabled(getSelectedProof() != null);
         addKeYSelectionListener(new KeYSelectionListener() {
 
             @Override
             public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
-                a.setEnabled(e.getSource().getSelectedProof() != null);
+                a.setEnabled(e.source().getSelectedProof() != null);
             }
         });
     }

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

@@ -6,52 +6,20 @@
 
 /**
  * An event that indicates that the users focused node or proof has changed
+ *
+ * @param source            the source of this event
+ * @param previousSelection the previously selected item
+ * @param currentSelection  the previously selected item
  */
-
-public class KeYSelectionEvent<Sel> {
-
-    /** the source of this event */
-    private final KeYSelectionModel source;
-
-    /** the previously selected item */
-    private final Sel previousSelection;
-
-    /**
-     * creates a new SelectedNodeEvent
-     *
-     * @param source the SelectedNodeModel where the event had its origin
-     * @param previousSelection the previous selected item
-     */
-    public KeYSelectionEvent(KeYSelectionModel source, Sel previousSelection) {
-        this.source = source;
-        this.previousSelection = previousSelection;
-    }
-
-    /**
-     * creates a new SelectedNodeEvent
-     *
-     * @param source the SelectedNodeModel where the event had its origin
-     */
-    public KeYSelectionEvent(KeYSelectionModel source) {
-        this(source, null);
-    }
-
-
+public record KeYSelectionEvent<Sel>(
+        KeYSelectionModel source, Sel previousSelection, Sel currentSelection) {
     /**
      * returns the KeYSelectionModel that caused this event
      *
      * @return the KeYSelectionModel that caused this event
      */
-    public KeYSelectionModel getSource() {
+    @Override
+    public KeYSelectionModel source() {
         return source;
     }
-
-    /**
-     * returns the previous selected item
-     *
-     * @return the previous selected item
-     */
-    public Sel getPreviousSelection() {
-        return previousSelection;
-    }
 }

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

@@ -360,7 +360,7 @@ public void removeKeYSelectionListener(KeYSelectionListener listener) {
     public synchronized void fireSelectedNodeChanged(Node previousNode) {
         synchronized (listenerList) {
             final KeYSelectionEvent<Node> selectionEvent =
-                new KeYSelectionEvent<>(this, previousNode);
+                new KeYSelectionEvent<>(this, previousNode, selectedNode);
             for (final KeYSelectionListener listener : listenerList) {
                 listener.selectedNodeChanged(selectionEvent);
             }
@@ -371,7 +371,7 @@ public synchronized void fireSelectedProofChanged(Proof previousProof) {
         synchronized (listenerList) {
             LOGGER.debug("Selected Proof changed, firing...");
             final KeYSelectionEvent<Proof> selectionEvent =
-                new KeYSelectionEvent<>(this, previousProof);
+                new KeYSelectionEvent<>(this, previousProof, proof);
             for (final KeYSelectionListener listener : listenerList) {
                 listener.selectedProofChanged(selectionEvent);
             }

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

@@ -568,7 +568,7 @@ public void selectedNodeChanged(KeYSelectionEvent<Node> e) {
          */
         public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
             LOGGER.debug("GoalList: initialize with new proof");
-            selectingListModel.setProof(e.getSource().getSelectedProof());
+            selectingListModel.setProof(e.source().getSelectedProof());
             validate();
         }
     }

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

@@ -214,7 +214,7 @@ public void selectedNodeChanged(KeYSelectionEvent<Node> e) {
          */
         @Override
         public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
-            final KeYSelectionModel selectionModel = e.getSource();
+            final KeYSelectionModel selectionModel = e.source();
             Runnable action = () -> {
                 if (isVisible()) {
                     if (selectionModel.getSelectedProof() == null) {