From a5f595a1a87506b4c131738e48a2e38a2c65ef11 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 22 Jun 2026 15:06:18 +0200 Subject: [PATCH 1/6] automode to choose from a dropdown list --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 125 +++++++++++++++++- .../ilkd/key/gui/actions/AutoModeAction.java | 9 +- .../gui/actions/MacroAutomationAction.java | 74 +++++++++++ .../ilkd/key/gui/fonticons/IconFactory.java | 97 ++++++++++++++ 4 files changed, 299 insertions(+), 6 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 140604cd34f..316bc93a96f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -240,6 +240,7 @@ public final class MainWindow extends JFrame { private ChangeListener selectAllListener; private JCheckBoxMenuItem selectAll; private JSeparator separator; + private DropdownSelectionButton automationComponent; private ExitMainAction exitMainAction; private ShowActiveSettingsAction showActiveSettingsAction; private UnicodeToggleAction unicodeToggleAction; @@ -283,6 +284,12 @@ public final class MainWindow extends JFrame { private final LruCached highlightCache = new LruCached<>(HTMLSyntaxHighlighter.Args::run); + /** + * List of automation actions for the dropdown button. + * To add new automation modes, add them to {@link #createAutomationActions()}. + */ + private final List automationActions; + /* * This class should only be instantiated once! */ @@ -329,6 +336,19 @@ private MainWindow() { strategySelectionView = new StrategySelectionView(this, mediator); openGoalsView = new GoalList(mediator); + // Initialize automation actions + automationActions = createAutomationActions(); + + // Register keyboard shortcut for default automation action (Ctrl+Space) + if (!automationActions.isEmpty()) { + Action defaultAction = automationActions.get(0); + KeyStroke accelerator = (KeyStroke) defaultAction.getValue(Action.ACCELERATOR_KEY); + if (accelerator != null) { + inputMap.put(accelerator, "defaultAutomation"); + getRootPane().getActionMap().put("defaultAutomation", defaultAction); + } + } + layoutMain(); SwingUtilities.updateComponentTreeUI(this); ToolTipManager.sharedInstance().setDismissDelay(30000); @@ -652,7 +672,9 @@ private JToolBar createProofControlToolBar() { toolBar.setFloatable(false); toolBar.setRollover(true); - toolBar.add(createWiderAutoModeButton()); + DropdownSelectionButton autoComp = createAutomationComponent(); + toolBar.add(autoComp.getActionComponent()); + toolBar.add(autoComp.getSelectionComponent()); toolBar.addSeparator(); toolBar.addSeparator(); toolBar.addSeparator(); @@ -748,6 +770,100 @@ private DropdownSelectionButton createSMTComponent() { return smtComponent; } + // @formatter:off + /** + * Creates the list of automation actions for the dropdown button. + *

+ * The first action in the list is the default and will be triggered by the {@code Ctrl+Space} + * keyboard shortcut. Actions are displayed in the dropdown menu in the order they are added. + *

+ *

+ * To add new automation modes, simply add them to this list. No configuration file or service + * loader is needed. For macro-based automations, use {@link MacroAutomationAction}. For custom + * behaviors, extend {@link MainWindowAction}. + *

+ *

+ * Example: + * + * 

+     * {@code
+     * actions.add(new MacroAutomationAction(this,
+     *     new YourCustomMacro(),
+     *     "Your Automation Name",
+     *     IconFactory.yourIcon(TOOLBAR_ICON_SIZE)));
+     * }
+     *
+ *

+ * + * @return list of automation actions + * @see MacroAutomationAction + * @see RunAutomationAction + */ + // @formatter:on + private List createAutomationActions() { + List actions = new ArrayList<>(); + + // Legacy default action (first item = default, triggered by Ctrl+Space) + actions.add(new RunAutomationAction(this)); + + // Full Auto Pilot: Finish symbolic execution, separate obligations, expand invariants, try + // close + actions.add(new MacroAutomationAction(this, + new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(), + "Full Auto Pilot", + IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE))); + + // Prepare-only Auto Pilot: Same as Full Auto Pilot but without trying to close goals + actions.add(new MacroAutomationAction(this, + new de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro(), + "Prepare-only Autopilot", + IconFactory.automationPrepareLogo(TOOLBAR_ICON_SIZE))); + + // Add new automation actions here: + // actions.add(new YourNewAutomationAction(this)); + + return actions; + } + + /** + * Create the automation component dropdown button. + * This replaces the old auto mode button with a configurable dropdown selector. + * + * @return the automation {@link DropdownSelectionButton} + */ + private DropdownSelectionButton createAutomationComponent() { + automationComponent = new DropdownSelectionButton(TOOLBAR_ICON_SIZE); + + // Convert list to array + Action[] actionArray = automationActions.toArray(new Action[0]); + + // Identity reducer - just return the single selected action + Function identityReducer = a -> { + if (a.length == 0) { + return null; + } + return a[0]; + }; + + // Set items with single selection (maxChoiceAmount = 1) + automationComponent.setItems(actionArray, identityReducer, 1); + + // Add change listener to update enabled state based on proof status + automationComponent.addListener(e -> { + Proof proof = mediator.getSelectedProof(); + boolean hasProof = proof != null && !proof.closed(); + automationComponent.setEnabled(hasProof); + }); + + // Initialize enabled state + Proof initialProof = mediator.getSelectedProof(); + automationComponent.setEnabled(initialProof != null && !initialProof.closed()); + + automationComponent.getActionComponent().putClientProperty("hideActionText", Boolean.TRUE); + + return automationComponent; + } + private JComponent createWiderAutoModeButton() { JButton b = new JButton(autoModeAction); b.putClientProperty("hideActionText", Boolean.TRUE); @@ -966,7 +1082,12 @@ public JMenu createProofMenu(Proof selected) { proof.setMnemonic(KeyEvent.VK_P); if (selected == null) { - proof.add(autoModeAction); + JMenu automationMenu = new JMenu("Automation"); + for (Action action : automationActions) { + JMenuItem item = new JMenuItem(action); + automationMenu.add(item); + } + proof.add(automationMenu); GoalBackAction goalBack = new GoalBackAction(this, true); proof.addMenuListener(new MenuListener() { @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java index 3a67ea35a12..e3294d5f471 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java @@ -25,11 +25,8 @@ public final class AutoModeAction extends MainWindowAction { private static final KeyStroke START_KEY = KeyStroke.getKeyStroke(KeyEvent.VK_SPACE, InputEvent.CTRL_DOWN_MASK); private static final KeyStroke STOP_KEY = KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0); - /** - * - */ private static final long serialVersionUID = -7702898691162947994L; - final Icon startLogo = IconFactory.autoModeStartLogo(MainWindow.TOOLBAR_ICON_SIZE); + final Icon startLogo = IconFactory.automationWithOverlay(MainWindow.TOOLBAR_ICON_SIZE, ""); final Icon stopLogo = IconFactory.autoModeStopLogo(MainWindow.TOOLBAR_ICON_SIZE); private Proof associatedProof; @@ -173,4 +170,8 @@ public void actionPerformed(ActionEvent e) { } } + @Override + public String toString() { + return "Full Automation"; + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java new file mode 100644 index 00000000000..8150bbb7728 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java @@ -0,0 +1,74 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.actions; + +import java.awt.event.ActionEvent; +import javax.swing.Icon; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.proof.Proof; + +/** + * Automation action that executes a proof macro. + *

+ * This is a reusable wrapper for macro-based automation actions. Instead of creating separate + * action classes for each macro, this generic wrapper can be used to expose any {@link ProofMacro} + * as an automation option in the dropdown menu. + *

+ *

+ * Example usage: + * + * 

+ * {@code
+ * actions.add(new MacroAutomationAction(mainWindow,
+ *     new FullAutoPilotProofMacro(),
+ *     "Full Auto Pilot",
+ *     IconFactory.automationFullPilotLogo(16)));
+ * }
+ *
+ *

+ * + * @see ProofMacro + * @see MainWindow#createAutomationActions() + */ +public class MacroAutomationAction extends MainWindowAction { + + private static final long serialVersionUID = 1L; + + /** The proof macro to execute when this action is triggered. */ + private final ProofMacro macro; + + /** + * Creates a new macro automation action. + * + * @param mainWindow the main window this action belongs to + * @param macro the proof macro to execute + * @param name the display name shown in the dropdown menu + * @param icon the icon displayed on the action button + */ + public MacroAutomationAction(MainWindow mainWindow, ProofMacro macro, String name, Icon icon) { + super(mainWindow); + this.macro = macro; + putValue(NAME, name); + putValue(SHORT_DESCRIPTION, macro.getDescription()); + putValue(SMALL_ICON, icon); + } + + @Override + public void actionPerformed(ActionEvent e) { + if (!getMediator().isInAutoMode()) { + Proof proof = getMediator().getSelectedProof(); + if (proof != null && !proof.closed()) { + getMediator().getUI().getProofControl() + .runMacro(getMediator().getSelectedNode(), macro, null); + } + } + } + + @Override + public String toString() { + return (String) getValue(NAME); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java index 9c149e44ccf..90f9c797c0e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.gui.fonticons; import java.awt.*; +import java.awt.image.BufferedImage; import java.net.URL; import java.util.ArrayList; import java.util.HashMap; @@ -366,6 +367,102 @@ public static Icon autoModeStopLogo(int size) { return AUTO_MODE_STOP.load(size); } + /** + * Creates an icon with a play button and a letter overlay. + *

+ * Used for automation actions to distinguish different modes visually. The base icon is the + * standard green play button ({@link #autoModeStartLogo(int)}), with a bold italic letter + * overlaid in the bottom-right corner. + *

+ * + * @param size the size of the icon in pixels + * @param letter the letter to overlay (e.g., "R" for Run, "F" for Full, "P" for Prepare), or + * {@code null} for just the play button + * @return the composite icon with letter overlay + * @see #automationRunLogo(int) + * @see #automationFullPilotLogo(int) + * @see #automationPrepareLogo(int) + */ + public static Icon automationWithOverlay(int size, String letter) { + Icon baseIcon = autoModeStartLogo(size); + + BufferedImage image = new BufferedImage(size + 5, size, BufferedImage.TYPE_INT_ARGB); + Graphics2D g2d = image.createGraphics(); + g2d.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON); + g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, + RenderingHints.VALUE_TEXT_ANTIALIAS_LCD_HRGB); + + // Draw base icon + baseIcon.paintIcon(null, g2d, 0, 0); + + if (letter == null) { + return new ImageIcon(image); + } + + // Draw letter overlay + g2d.setColor(Color.BLACK); + Font font = new Font(Font.SANS_SERIF, Font.BOLD | Font.ITALIC, (int) (size * 0.9f)); + g2d.setFont(font); + + FontMetrics fm = g2d.getFontMetrics(); + int textWidth = fm.stringWidth(letter); + int textHeight = fm.getAscent() - fm.getDescent(); + + // Position letter in bottom-right corner + int x = size - textWidth; + + g2d.drawString(letter, x + 5, size); + g2d.dispose(); + + return new ImageIcon(image); + } + + /** + * Creates an icon for the "Run Automation" action. + *

+ * This is the legacy default automation mode that starts/stops automated proof search. + * The icon shows a green play button with an "R" overlay. + *

+ * + * @param size the size of the icon in pixels + * @return the automation run icon + */ + public static Icon automationRunLogo(int size) { + return automationWithOverlay(size, "R"); + } + + /** + * Creates an icon for the "Full Auto Pilot" action. + *

+ * This automation mode performs: finish symbolic execution, separate proof obligations, expand + * invariant definitions, and try to close all proof obligations. + * The icon shows a green play button with an "F" overlay. + *

+ * + * @param size the size of the icon in pixels + * @return the full auto pilot icon + * @see de.uka.ilkd.key.macros.FullAutoPilotProofMacro + */ + public static Icon automationFullPilotLogo(int size) { + return automationWithOverlay(size, "F"); + } + + /** + * Creates an icon for the "Prepare-only Autopilot" action. + *

+ * This automation mode performs: finish symbolic execution, separate proof obligations, and + * expand invariant definitions (without trying to close goals). + * The icon shows a green play button with a "P" overlay. + *

+ * + * @param size the size of the icon in pixels + * @return the prepare-only autopilot icon + * @see de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro + */ + public static Icon automationPrepareLogo(int size) { + return automationWithOverlay(size, "P"); + } + public static Icon selectDecProcArrow(int size) { // return scaleIcon(decisionProcedureConfigArrow, size / 2, size); return CONFIGURE_MENU.load(size); From 1b09b1d0fe5333eb8f30b3a378c916260d16d62e Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 22 Jun 2026 18:22:06 +0200 Subject: [PATCH 2/6] repairing missing links and stop capabilities --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 36 +++++------------ .../ilkd/key/gui/actions/AutoModeAction.java | 12 ++++-- .../gui/actions/MacroAutomationAction.java | 40 +++++++------------ 3 files changed, 34 insertions(+), 54 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 316bc93a96f..620cc170156 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -797,32 +797,17 @@ private DropdownSelectionButton createSMTComponent() { * * @return list of automation actions * @see MacroAutomationAction - * @see RunAutomationAction + * @see AutoModeAction */ // @formatter:on private List createAutomationActions() { - List actions = new ArrayList<>(); - - // Legacy default action (first item = default, triggered by Ctrl+Space) - actions.add(new RunAutomationAction(this)); - - // Full Auto Pilot: Finish symbolic execution, separate obligations, expand invariants, try - // close - actions.add(new MacroAutomationAction(this, - new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(), - "Full Auto Pilot", - IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE))); - - // Prepare-only Auto Pilot: Same as Full Auto Pilot but without trying to close goals - actions.add(new MacroAutomationAction(this, - new de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro(), - "Prepare-only Autopilot", - IconFactory.automationPrepareLogo(TOOLBAR_ICON_SIZE))); - - // Add new automation actions here: - // actions.add(new YourNewAutomationAction(this)); - - return actions; + return List.of(new AutoModeAction(this), + new MacroAutomationAction(this, + new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(), + IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE)), + new MacroAutomationAction(this, + new de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro(), + IconFactory.automationPrepareLogo(TOOLBAR_ICON_SIZE))); } /** @@ -860,6 +845,7 @@ private DropdownSelectionButton createAutomationComponent() { automationComponent.setEnabled(initialProof != null && !initialProof.closed()); automationComponent.getActionComponent().putClientProperty("hideActionText", Boolean.TRUE); + automationComponent.getActionComponent().putClientProperty("isAutoButton", Boolean.TRUE); return automationComponent; } @@ -1732,8 +1718,8 @@ 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())) { + if (c instanceof JComponent jc + && jc.getClientProperty("isAutoButton") == Boolean.TRUE) { return true; } c = c.getParent(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java index e3294d5f471..2a8405da7d9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java @@ -18,16 +18,17 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.*; +import org.jspecify.annotations.NonNull; import org.key_project.util.collection.ImmutableList; -public final class AutoModeAction extends MainWindowAction { +public class AutoModeAction extends MainWindowAction { private static final KeyStroke START_KEY = KeyStroke.getKeyStroke(KeyEvent.VK_SPACE, InputEvent.CTRL_DOWN_MASK); private static final KeyStroke STOP_KEY = KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0); private static final long serialVersionUID = -7702898691162947994L; - final Icon startLogo = IconFactory.automationWithOverlay(MainWindow.TOOLBAR_ICON_SIZE, ""); - final Icon stopLogo = IconFactory.autoModeStopLogo(MainWindow.TOOLBAR_ICON_SIZE); + private final Icon startLogo; + private final Icon stopLogo = IconFactory.autoModeStopLogo(MainWindow.TOOLBAR_ICON_SIZE); private Proof associatedProof; @@ -60,11 +61,16 @@ public void proofGoalsAdded(ProofTreeEvent e) { }; public AutoModeAction(MainWindow mainWindow) { + this(mainWindow, IconFactory.automationWithOverlay(MainWindow.TOOLBAR_ICON_SIZE, "")); + } + + public AutoModeAction(MainWindow mainWindow, Icon startLogo) { super(mainWindow); associatedProof = getMediator().getSelectedProof(); putValue("hideActionText", Boolean.TRUE); setName(getStartCommand()); setTooltip(MainWindow.AUTO_MODE_TEXT); + this.startLogo = startLogo; setIcon(startLogo); enable(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java index 8150bbb7728..540f5b66d56 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java @@ -6,9 +6,13 @@ import java.awt.event.ActionEvent; import javax.swing.Icon; +import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.useractions.ProofMacroUserAction; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import org.key_project.prover.engine.TaskStartedInfo; /** * Automation action that executes a proof macro. @@ -17,23 +21,10 @@ * action classes for each macro, this generic wrapper can be used to expose any {@link ProofMacro} * as an automation option in the dropdown menu. *

- *

- * Example usage: - * - * 

- * {@code
- * actions.add(new MacroAutomationAction(mainWindow,
- *     new FullAutoPilotProofMacro(),
- *     "Full Auto Pilot",
- *     IconFactory.automationFullPilotLogo(16)));
- * }
- *
- *

* * @see ProofMacro - * @see MainWindow#createAutomationActions() */ -public class MacroAutomationAction extends MainWindowAction { +public class MacroAutomationAction extends AutoModeAction { private static final long serialVersionUID = 1L; @@ -45,25 +36,22 @@ public class MacroAutomationAction extends MainWindowAction { * * @param mainWindow the main window this action belongs to * @param macro the proof macro to execute - * @param name the display name shown in the dropdown menu * @param icon the icon displayed on the action button */ - public MacroAutomationAction(MainWindow mainWindow, ProofMacro macro, String name, Icon icon) { - super(mainWindow); + public MacroAutomationAction(MainWindow mainWindow, ProofMacro macro, Icon icon) { + super(mainWindow, icon); this.macro = macro; - putValue(NAME, name); - putValue(SHORT_DESCRIPTION, macro.getDescription()); - putValue(SMALL_ICON, icon); + setName(macro.getName()); + setTooltip(macro.getDescription()); } @Override public void actionPerformed(ActionEvent e) { - if (!getMediator().isInAutoMode()) { - Proof proof = getMediator().getSelectedProof(); - if (proof != null && !proof.closed()) { - getMediator().getUI().getProofControl() - .runMacro(getMediator().getSelectedNode(), macro, null); - } + KeYMediator mediator = getMediator(); + if (mediator.isInAutoMode()) { + getMediator().getUI().getProofControl().stopAutoMode(); + } else { + mediator.getUI().getProofControl().runMacro(mediator.getSelectedNode(), macro, null); } } From 1c298498b6e3d490c7e430c13ef8c3f9f874c713 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 22 Jun 2026 22:10:27 +0200 Subject: [PATCH 3/6] spotless, improved cursor behaviour --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 25 ++++++++++++------- .../ilkd/key/gui/actions/AutoModeAction.java | 1 - .../gui/actions/MacroAutomationAction.java | 4 --- 3 files changed, 16 insertions(+), 14 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 620cc170156..b6557736556 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -802,12 +802,12 @@ private DropdownSelectionButton createSMTComponent() { // @formatter:on private List createAutomationActions() { return List.of(new AutoModeAction(this), - new MacroAutomationAction(this, - new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(), - IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE)), - new MacroAutomationAction(this, - new de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro(), - IconFactory.automationPrepareLogo(TOOLBAR_ICON_SIZE))); + new MacroAutomationAction(this, + new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(), + IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE)), + new MacroAutomationAction(this, + new de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro(), + IconFactory.automationPrepareLogo(TOOLBAR_ICON_SIZE))); } /** @@ -1706,10 +1706,17 @@ private void redispatchMouseEvent(MouseEvent e) { Component component = SwingUtilities.getDeepestComponentAt(contentPane, containerPoint.x, containerPoint.y); - if (eventID == MouseEvent.MOUSE_PRESSED && isLiveComponent(component)) { - currentComponent = component; - dispatchForCurrentComponent(e); + if (isLiveComponent(component)) { + if (eventID == MouseEvent.MOUSE_PRESSED) { + currentComponent = component; + dispatchForCurrentComponent(e); + } + glassPane.setCursor(new Cursor(Cursor.DEFAULT_CURSOR)); + } else { + glassPane.setCursor(new Cursor(Cursor.WAIT_CURSOR)); } + + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java index 2a8405da7d9..5430da3a75e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java @@ -18,7 +18,6 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.*; -import org.jspecify.annotations.NonNull; import org.key_project.util.collection.ImmutableList; public class AutoModeAction extends MainWindowAction { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java index 540f5b66d56..138e2b2ad32 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroAutomationAction.java @@ -8,11 +8,7 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.actions.useractions.ProofMacroUserAction; import de.uka.ilkd.key.macros.ProofMacro; -import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; -import org.key_project.prover.engine.TaskStartedInfo; /** * Automation action that executes a proof macro. From 7ad6ecebc6b5531a692ffc490183ffbde44931cf Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 23 Jun 2026 13:51:15 +0200 Subject: [PATCH 4/6] Introducing a legacy default apply strategy macro --- .../uka/ilkd/key/macros/DefaultAutoMacro.java | 89 +++++++++++++++++++ .../de.uka.ilkd.key.macros.ProofMacro | 1 + 2 files changed, 90 insertions(+) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java new file mode 100644 index 00000000000..a11686ed825 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java @@ -0,0 +1,89 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.macros; + +import java.util.List; +import java.util.stream.Collectors; + +import de.uka.ilkd.key.control.UserInterfaceControl; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.prover.impl.ApplyStrategy; + +import org.key_project.prover.engine.GoalChooser; +import org.key_project.prover.engine.ProverCore; +import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +/** + * The macro {@link DefaultAutoMacro} runs the active proof strategy on all enabled goals + * in the selected subtree. This is equivalent to pressing the Auto button but can be + * invoked from context menus or keyboard shortcuts. + * + * This is used to show traditional strategy application as an item in the context menus. + * + * @author mattias ulbrich + */ +public class DefaultAutoMacro extends AbstractProofMacro { + + @Override + public String getName() { + return "Apply Strategy"; + } + + @Override + public String getCategory() { + return "Auto Pilot"; + } + + @Override + public String getScriptCommandName() { + return "auto"; + } + + @Override + public String getDescription() { + return "Runs the active proof strategy on the selected subtree (same as Auto button)"; + } + + @Override + public boolean canApplyTo(Proof proof, ImmutableList goals, + PosInOccurrence posInOcc) { + return goals != null && !goals.isEmpty(); + } + + @Override + public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, + ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) + throws InterruptedException { + if (goals == null || goals.isEmpty()) { + return null; + } + + List nodes = goals.stream().map(Goal::node).collect(Collectors.toList()); + + final GoalChooser goalChooser = + proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create(); + final ProverCore applyStrategy = new ApplyStrategy(goalChooser); + + final ProofMacroListener pml = + new ProgressBarListener(goals.size(), getMaxSteps(proof), listener); + applyStrategy.addProverTaskObserver(pml); + + try { + applyStrategy.start(proof, goals); + synchronized (applyStrategy) { + if (applyStrategy.hasBeenInterrupted()) { + throw new InterruptedException(); + } + } + } finally { + applyStrategy.removeProverTaskObserver(pml); + } + + return new ProofMacroFinishedInfo(this, proof.openGoals(), nodes); + } +} diff --git a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro index 861bc5b2e03..6a853efcc14 100644 --- a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro +++ b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro @@ -4,6 +4,7 @@ # # warning: subject to change of package name +de.uka.ilkd.key.macros.DefaultAutoMacro de.uka.ilkd.key.macros.FullAutoPilotProofMacro #de.uka.ilkd.key.macros.FullAutoPilotWithJMLSpecJoinsProofMacro de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro From 29846bc630b6b8b27e330fe6cf7a1dcc4b9a9181 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 23 Jun 2026 13:51:29 +0200 Subject: [PATCH 5/6] removing dead code from the icon factory --- .../de/uka/ilkd/key/gui/fonticons/IconFactory.java | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java index 90f9c797c0e..a1f2ceb56ef 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java @@ -417,20 +417,6 @@ public static Icon automationWithOverlay(int size, String letter) { return new ImageIcon(image); } - /** - * Creates an icon for the "Run Automation" action. - *

- * This is the legacy default automation mode that starts/stops automated proof search. - * The icon shows a green play button with an "R" overlay. - *

- * - * @param size the size of the icon in pixels - * @return the automation run icon - */ - public static Icon automationRunLogo(int size) { - return automationWithOverlay(size, "R"); - } - /** * Creates an icon for the "Full Auto Pilot" action. *

From a4943615e680a66f1f83fa32e3ae45c30b5b6774 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 23 Jun 2026 19:35:05 +0200 Subject: [PATCH 6/6] Improved the UX by more tooltips and clearer names and descriptions --- .../ilkd/key/macros/AutoPilotPrepareProofMacro.java | 11 ++++++++--- .../de/uka/ilkd/key/macros/DefaultAutoMacro.java | 5 +++-- .../uka/ilkd/key/macros/FullAutoPilotProofMacro.java | 12 +++++++++--- .../main/java/de/uka/ilkd/key/gui/MainWindow.java | 6 +++++- .../ilkd/key/gui/smt/DropdownSelectionButton.java | 1 + 5 files changed, 26 insertions(+), 9 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AutoPilotPrepareProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AutoPilotPrepareProofMacro.java index 35db994b6cf..43608bf2664 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/AutoPilotPrepareProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/AutoPilotPrepareProofMacro.java @@ -36,7 +36,7 @@ public class AutoPilotPrepareProofMacro extends StrategyProofMacro { @Override public String getName() { - return "Auto Pilot (Preparation Only)"; + return "Structured Automation (Prep. Only)"; } @Override @@ -46,8 +46,13 @@ public String getCategory() { @Override public String getDescription() { - return "

  1. Finish symbolic execution" + "
  2. Separate proof obligations" - + "
  3. Expand invariant definitions
"; + return "This configures the automation such that it preserves
" + + "the program structure and makes it easier to comprehend the
" + + "resulting proof. It produces proof goals without program
" + + "references, but does not try to close these goals.
" + + "The steps are:
  1. Finish symbolic execution" + + "
  2. Separate proof obligations" + + "
  3. Expand invariant definitions
"; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java index a11686ed825..e8efea54c3e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/DefaultAutoMacro.java @@ -31,7 +31,7 @@ public class DefaultAutoMacro extends AbstractProofMacro { @Override public String getName() { - return "Apply Strategy"; + return "Full Automation"; } @Override @@ -46,7 +46,8 @@ public String getScriptCommandName() { @Override public String getDescription() { - return "Runs the active proof strategy on the selected subtree (same as Auto button)"; + return "Runs the full proof strategy on the selected subtree.
" + + "The strategy can be configured in 'Proof Search Strategy' tab."; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java index c0b3c098957..1291127fdc8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java @@ -29,7 +29,7 @@ public class FullAutoPilotProofMacro extends SequentialProofMacro { @Override public String getName() { - return "Full Auto Pilot"; + return "Structured Automation"; } @Override @@ -44,8 +44,14 @@ public String getScriptCommandName() { @Override public String getDescription() { - return "
  1. Finish symbolic execution" + "
  2. Separate proof obligations" - + "
  3. Expand invariant definitions" + "
  4. Try to close all proof obligations
"; + return "This configures the automation such that it preserves
" + + "the program structure and makes it easier to comprehend the
" + + "resulting proof.
" + + "The steps are:" + + "
  1. Finish symbolic execution" + + "
  2. Separate proof obligations" + + "
  3. Expand invariant definitions" + + "
  4. Try to close all proof obligations
"; } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index b6557736556..cd1add14165 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -55,6 +55,7 @@ import de.uka.ilkd.key.gui.smt.DropdownSelectionButton; import de.uka.ilkd.key.gui.sourceview.SourceViewFrame; import de.uka.ilkd.key.gui.utilities.LruCached; +import de.uka.ilkd.key.macros.DefaultAutoMacro; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.io.ProblemLoader; @@ -801,7 +802,10 @@ private DropdownSelectionButton createSMTComponent() { */ // @formatter:on private List createAutomationActions() { - return List.of(new AutoModeAction(this), + return List.of( + new MacroAutomationAction(this, + new DefaultAutoMacro(), + IconFactory.automationWithOverlay(TOOLBAR_ICON_SIZE, "")), new MacroAutomationAction(this, new de.uka.ilkd.key.macros.FullAutoPilotProofMacro(), IconFactory.automationFullPilotLogo(TOOLBAR_ICON_SIZE)), diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/DropdownSelectionButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/DropdownSelectionButton.java index f7e3ffab964..ca2539bbd65 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/DropdownSelectionButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/DropdownSelectionButton.java @@ -397,6 +397,7 @@ public void setItems(Action[] it, Function reduce, int maxChoi } menuItem.setEnabled(true); menuItem.setText(item.toString()); + menuItem.setToolTipText(item.getValue(Action.SHORT_DESCRIPTION).toString()); menuItem.putClientProperty("CheckBoxMenuItem.doNotCloseOnMouseClick", Boolean.TRUE); menuItems.add(menuItem); }