start with fixing #3415

Author: wadoon

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

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,15 +705,21 @@ 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 e) {
+            public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
                 a.setEnabled(e.getSource().getSelectedProof() != null);
             }
         });
@@ -722,13 +729,13 @@ public void selectedProofChanged(KeYSelectionEvent 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 e) {
+            public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
                 a.setEnabled(e.getSource().getSelectedProof() != null);
             }
         });

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

@@ -6,11 +6,10 @@
 import java.awt.*;
 import java.awt.event.ActionEvent;
 import java.awt.event.KeyEvent;
-import java.awt.event.KeyListener;
-import java.awt.event.MouseEvent;
 import java.beans.PropertyChangeEvent;
 import java.beans.PropertyChangeListener;
 import java.io.File;
+import java.lang.reflect.Field;
 import java.lang.reflect.InvocationTargetException;
 import java.lang.reflect.Method;
 import java.util.*;
@@ -24,7 +23,6 @@
 import javax.swing.event.ChangeListener;
 import javax.swing.event.MenuEvent;
 import javax.swing.event.MenuListener;
-import javax.swing.event.MouseInputAdapter;
 
 import de.uka.ilkd.key.control.AutoModeListener;
 import de.uka.ilkd.key.control.TermLabelVisibilityManager;
@@ -57,6 +55,7 @@
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.ProofAggregate;
 import de.uka.ilkd.key.proof.ProofEvent;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.settings.FeatureSettings;
@@ -106,6 +105,8 @@ public final class MainWindow extends JFrame {
         "Activates the 'Run All Proofs' action that allows you to run multiple proofs inside the UI.",
         false);
 
+    public static final String PROPERTY_IN_AUTO_MODE = "inAutoMode";
+
     private static MainWindow instance = null;
     /**
      * Search bar for Sequent Views.
@@ -167,23 +168,27 @@ public final class MainWindow extends JFrame {
     private final ToggleProofTreeTooltipAction toogleProofTreeTooltipAction =
         new ToggleProofTreeTooltipAction(this);
     private final TermLabelMenu termLabelMenu;
-    private boolean frozen = false;
+
     /**
      *
      */
     private final CControl dockControl = new CControl(this);
+
     /**
      * the first toolbar
      */
     private JToolBar controlToolBar;
+
     /**
      * the second toolbar
      */
     private JToolBar fileOpToolBar;
+
     /**
      * the status line
      */
     private MainStatusLine statusLine;
+
     /**
      * action for opening a KeY file
      */
@@ -278,6 +283,7 @@ public final class MainWindow extends JFrame {
 
     private final LruCached<HTMLSyntaxHighlighter.Args, String> highlightCache =
         new LruCached<>(HTMLSyntaxHighlighter.Args::run);
+    private boolean inAutoMode;
 
     /*
      * This class should only be instantiated once!
@@ -442,7 +448,7 @@ public TermLabelVisibilityManager getVisibleTermLabels() {
      */
     private void applyGnomeWorkaround() {
         Toolkit xToolkit = Toolkit.getDefaultToolkit();
-        java.lang.reflect.Field awtAppClassNameField;
+        Field awtAppClassNameField;
         try {
             awtAppClassNameField = xToolkit.getClass().getDeclaredField("awtAppClassName");
             awtAppClassNameField.setAccessible(true);
@@ -573,7 +579,7 @@ private void layoutMain() {
 
         getContentPane().add(toolBarPanel, BorderLayout.PAGE_START);
 
-        proofListView.setPreferredSize(new java.awt.Dimension(350, 100));
+        proofListView.setPreferredSize(new Dimension(350, 100));
         GuiUtilities.paintEmptyViewComponent(proofListView, "Proofs");
 
         // JSplitPane leftPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, proofListView,
@@ -815,27 +821,6 @@ public void setStatusLine(final String str, final int max) {
         ThreadUtilities.invokeOnEventQueue(() -> setStatusLineImmediately(str, max));
     }
 
-    /**
-     * Freeze the main window by blocking all input events, except those for the toolbar (i.e.
-     * the abort button within the toolbar)
-     */
-    public void freezeExceptAutoModeButton() {
-        if (!frozen) {
-            frozen = true;
-
-            Component glassPane = new BlockingGlassPane(getContentPane());
-            setGlassPane(glassPane);
-            glassPane.setVisible(true);
-        }
-    }
-
-    public void unfreezeExceptAutoModeButton() {
-        if (frozen) {
-            getGlassPane().setVisible(false);
-            frozen = false;
-        }
-    }
-
     /**
      * Update the sequent view.
      */
@@ -846,7 +831,7 @@ public void makePrettyView() {
         SwingUtilities.invokeLater(this::updateSequentView);
     }
 
-    private void addToProofList(de.uka.ilkd.key.proof.ProofAggregate plist) {
+    private void addToProofList(ProofAggregate plist) {
         proofList.addProof(plist);
         // TODO/Check: the code below emulates phantom actions. Check if this can be solved
         // differently
@@ -1183,7 +1168,7 @@ public CurrentGoalView getGoalView() {
         return currentGoalView;
     }
 
-    public void addProblem(final de.uka.ilkd.key.proof.ProofAggregate plist) {
+    public void addProblem(final ProofAggregate plist) {
         Runnable guiUpdater = () -> {
             disableCurrentGoalView = true;
             addToProofList(plist);
@@ -1489,146 +1474,14 @@ public CurrentGoalView getCurrentGoalView() {
         return currentGoalView;
     }
 
-    /**
-     * Glass pane that only delivers events for the status line (i.e. the abort button)
-     * <p>
-     * This has been partly taken from the GlassPaneDemo of the Java Tutorial
-     */
-    private static class BlockingGlassPane extends JComponent {
-        /**
-         *
-         */
-        private static final long serialVersionUID = 1218022319090988424L;
-        private final GlassPaneListener listener;
-
-        public BlockingGlassPane(Container contentPane) {
-            setCursor(new Cursor(Cursor.WAIT_CURSOR));
-
-            listener = new GlassPaneListener(this, contentPane);
-            addMouseListener(listener);
-            addMouseMotionListener(listener);
-            addKeyListener(new KeyListener() {
-
-                @Override
-                public void keyPressed(KeyEvent e) {
-                    e.consume();
-                }
-
-                @Override
-                public void keyReleased(KeyEvent e) {
-                    e.consume();
-
-                }
-
-                @Override
-                public void keyTyped(KeyEvent e) {
-                    e.consume();
-                }
-
-            });
-        }
+    public void setInAutoMode(boolean inAutoMode) {
+        var oldValue = this.inAutoMode;
+        this.inAutoMode = inAutoMode;
+        firePropertyChange(PROPERTY_IN_AUTO_MODE, oldValue, inAutoMode);
     }
 
-    /**
-     * Mouse listener for the glass pane that only delivers events for the status line (i.e. the
-     * abort button)
-     * <p>
-     * This has been partly taken from the GlassPaneDemo of the Java Tutorial
-     */
-    private static class GlassPaneListener extends MouseInputAdapter {
-        Component currentComponent = null;
-        final Component glassPane;
-        final Container contentPane;
-
-        public GlassPaneListener(Component glassPane, Container contentPane) {
-            this.glassPane = glassPane;
-            this.contentPane = contentPane;
-        }
-
-        @Override
-        public void mouseMoved(MouseEvent e) {
-            redispatchMouseEvent(e);
-        }
-
-        /*
-         * We must forward at least the mouse drags that started with mouse presses over the check
-         * box. Otherwise, when the user presses the check box then drags off, the check box isn't
-         * disarmed -- it keeps its dark gray background or whatever its L&F uses to indicate that
-         * the button is currently being pressed.
-         */
-        @Override
-        public void mouseDragged(MouseEvent e) {
-            redispatchMouseEvent(e);
-        }
-
-        @Override
-        public void mouseClicked(MouseEvent e) {
-            redispatchMouseEvent(e);
-        }
-
-        @Override
-        public void mouseEntered(MouseEvent e) {
-            redispatchMouseEvent(e);
-        }
-
-        @Override
-        public void mouseExited(MouseEvent e) {
-            redispatchMouseEvent(e);
-        }
-
-        @Override
-        public void mousePressed(MouseEvent e) {
-            redispatchMouseEvent(e);
-        }
-
-        @Override
-        public void mouseReleased(MouseEvent e) {
-            redispatchMouseEvent(e);
-            currentComponent = null;
-        }
-
-        private void redispatchMouseEvent(MouseEvent e) {
-            if (currentComponent != null) {
-                dispatchForCurrentComponent(e);
-            } else {
-                int eventID = e.getID();
-                Point glassPanePoint = e.getPoint();
-
-                Point containerPoint =
-                    SwingUtilities.convertPoint(glassPane, glassPanePoint, contentPane);
-                Component component = SwingUtilities.getDeepestComponentAt(contentPane,
-                    containerPoint.x, containerPoint.y);
-
-                if (eventID == MouseEvent.MOUSE_PRESSED && isLiveComponent(component)) {
-                    currentComponent = component;
-                    dispatchForCurrentComponent(e);
-                }
-            }
-        }
-
-        // FIXME This is not really good.
-        private boolean isLiveComponent(Component c) {
-            // this is not the most elegant way to identify the right
-            // components, but it scales well ;-)
-            while (c != null) {
-                if ((c instanceof JComponent)
-                        && AUTO_MODE_TEXT.equals(((JComponent) c).getToolTipText())) {
-                    return true;
-                }
-                c = c.getParent();
-            }
-            return false;
-        }
-
-        private void dispatchForCurrentComponent(MouseEvent e) {
-            Point glassPanePoint = e.getPoint();
-            Point componentPoint =
-                SwingUtilities.convertPoint(glassPane, glassPanePoint, currentComponent);
-            currentComponent.dispatchEvent(new MouseEvent(currentComponent, e.getID(), e.getWhen(),
-                // do not use as it freezes the stop button: e.getModifiersEx(),
-                e.getModifiers(), componentPoint.x, componentPoint.y, e.getClickCount(),
-                e.isPopupTrigger()));
-        }
+    public boolean isInAutoMode() {
+        return inAutoMode;
     }
 
     /**
@@ -1776,7 +1629,7 @@ public synchronized void autoModeStarted(ProofEvent e) {
             LOGGER.debug("Automode started");
             disableCurrentGoalView = true;
             getMediator().removeKeYSelectionListener(proofListener);
-            freezeExceptAutoModeButton();
+            setInAutoMode(true);
         }
 
         /**
@@ -1785,9 +1638,9 @@ public synchronized void autoModeStarted(ProofEvent e) {
         @Override
         public synchronized void autoModeStopped(ProofEvent e) {
             LOGGER.debug("Automode stopped");
-            unfreezeExceptAutoModeButton();
             disableCurrentGoalView = false;
             getMediator().addKeYSelectionListenerChecked(proofListener);
+            setInAutoMode(false);
         }
 
         @Override

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AbandonTaskAction.java

@@ -24,7 +24,7 @@ public AbandonTaskAction(MainWindow mainWindow, Proof proof) {
         setIcon(IconFactory.abandon(16));
         setTooltip("Drop current proof.");
 
-        getMediator().enableWhenProofLoaded(this);
+        enabledOnAnActiveProof();
 
         this.proof = proof;
     }