Reduce clutter in toolbar

key.ui/build.gradle

@@ -27,7 +27,6 @@ dependencies {
     api 'org.dockingframes:docking-frames-core:1.1.3p1'
 
     runtimeOnly project(":keyext.ui.testgen")
-    runtimeOnly project(":keyext.action_history")
     runtimeOnly project(":keyext.exploration")
     runtimeOnly project(":keyext.slicing")
 }

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

@@ -43,6 +43,7 @@
 import de.uka.ilkd.key.gui.notification.NotificationManager;
 import de.uka.ilkd.key.gui.notification.events.ExitKeYEvent;
 import de.uka.ilkd.key.gui.notification.events.NotificationEvent;
+import de.uka.ilkd.key.gui.plugins.action_history.ActionHistoryExtension;
 import de.uka.ilkd.key.gui.proofdiff.ProofDiffFrame;
 import de.uka.ilkd.key.gui.prooftree.ProofTreeView;
 import de.uka.ilkd.key.gui.settings.SettingsManager;
@@ -621,6 +622,7 @@ private void layoutMain() {
 
     private JToolBar createFileOpsToolBar() {
         JToolBar fileOperations = new JToolBar("File Operations");
+        fileOperations.setFloatable(false);
         fileOperations.add(openFileAction);
         fileOperations.add(openMostRecentFileAction);
         fileOperations.add(editMostRecentFileAction);
@@ -634,7 +636,7 @@ private JToolBar createFileOpsToolBar() {
 
     private JToolBar createProofControlToolBar() {
         JToolBar toolBar = new JToolBar("Proof Control");
-        toolBar.setFloatable(true);
+        toolBar.setFloatable(false);
         toolBar.setRollover(true);
 
         toolBar.add(createWiderAutoModeButton());
@@ -647,6 +649,9 @@ private JToolBar createProofControlToolBar() {
         toolBar.addSeparator();
         toolBar.add(new GoalBackAction(this, false));
         toolBar.add(new PruneProofAction(this));
+        var act = new ActionHistoryExtension(this, mediator);
+        toolBar.add(act.getUndoButton().getAction());
+        toolBar.add(act.getUndoUptoButton());
         toolBar.addSeparator();
         // toolBar.add(createHeatmapToggle());
         // toolBar.add(createHeatmapMenuOpener());
@@ -656,7 +661,7 @@ private JToolBar createProofControlToolBar() {
 
     private JToolBar createNavigationToolBar() {
         JToolBar toolBar = new JToolBar("Selection Navigation");
-        toolBar.setFloatable(true);
+        toolBar.setFloatable(false);
         toolBar.setRollover(true);
 
         SelectionHistory history = new SelectionHistory(mediator);

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

@@ -152,6 +152,11 @@ public int getPriority() {
         return i == null ? 0 : i;
     }
 
+    /**
+     * Set the priority of this action. Actions are sorted from low priority to high priority.
+     *
+     * @param priority integer value
+     */
     protected void setPriority(int priority) {
         putValue(PRIORITY, priority);
     }

key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java

@@ -37,16 +37,15 @@
 @KeYGuiExtension.Info(name = "Docking Helpers", optional = false, experimental = false,
     priority = 1)
 public final class DockingLayout implements KeYGuiExtension, KeYGuiExtension.Startup,
-        KeYGuiExtension.MainMenu, KeYGuiExtension.Toolbar {
+        KeYGuiExtension.MainMenu {
     private static final Logger LOGGER = LoggerFactory.getLogger(DockingLayout.class);
 
     public static final float SIZE_ICON_DOCK = 12f;
     public static final File LAYOUT_FILE = new File(PathConfig.getKeyConfigDir(), "layout.xml");
-
     public static final String[] LAYOUT_NAMES = new String[] { "Default", "Slot 1", "Slot 2" };
-    public static final int[] LAYOUT_KEYS = new int[] { KeyEvent.VK_F11, KeyEvent.VK_F12 };
+    public static final int[] LAYOUT_KEYS =
+        new int[] { KeyEvent.VK_F10, KeyEvent.VK_F11, KeyEvent.VK_F12 };
 
-    private final List<Action> actions = new LinkedList<>();
     private MainWindow window;
 
     private void installIcons(MainWindow mw) {
@@ -90,18 +89,6 @@ private static void loadLayouts(CControl globalPort) {
         }
     }
 
-    private void ensureActions(MainWindow mw) {
-        if (actions.isEmpty()) {
-            int keypos = 0;
-            for (String layout : LAYOUT_NAMES) {
-                Integer key = keypos < LAYOUT_KEYS.length ? LAYOUT_KEYS[keypos] : null;
-                actions.add(new LoadLayoutAction(mw, layout, key));
-                actions.add(new SaveLayoutAction(mw, layout, key));
-                keypos++;
-            }
-        }
-    }
-
     @Override
     public void init(MainWindow window, KeYMediator mediator) {
         this.window = window;
@@ -135,69 +122,31 @@ private void setLayout(String layout) {
         boolean defaultLayoutDefined = Arrays.asList(globalPort.layouts()).contains(layout);
         if (defaultLayoutDefined) {
             globalPort.load(layout);
-            DockingHelper.restoreMissingPanels(window);
         }
-    }
-
-    @Override
-    public JToolBar getToolbar(MainWindow mainWindow) {
-        JToolBar toolBar = new JToolBar("Docking Layout");
-        JComboBox<String> comboLayouts = new JComboBox<>();
-
-        class SaveAction extends MainWindowAction {
-            private static final long serialVersionUID = -2688272657370615595L;
-
-            protected SaveAction(MainWindow mainWindow) {
-                super(mainWindow);
-                setName("Save Layout");
-            }
-
-            @Override
-            public void actionPerformed(ActionEvent e) {
-                String name = Objects.requireNonNull(comboLayouts.getSelectedItem()).toString();
-                mainWindow.getDockControl().save(name);
-            }
-        }
-
-        class LoadAction extends MainWindowAction {
-            private static final long serialVersionUID = 3130337190207622893L;
-
-            protected LoadAction(MainWindow mainWindow) {
-                super(mainWindow);
-                setName("Load Layout");
-            }
-
-            @Override
-            public void actionPerformed(ActionEvent e) {
-                setLayout(Objects.requireNonNull(comboLayouts.getSelectedItem()).toString());
-            }
-        }
-
-        toolBar.add(new JLabel("Layouts: "));
-        for (String s : LAYOUT_NAMES) {
-            comboLayouts.addItem(s);
-        }
-        toolBar.add(comboLayouts);
-        toolBar.add(new LoadAction(mainWindow));
-        toolBar.add(new SaveAction(mainWindow));
-        toolBar.addSeparator();
-        toolBar.add(new ResetLayoutAction(mainWindow));
-        return toolBar;
+        DockingHelper.restoreMissingPanels(window);
     }
 
     @Override
     public List<Action> getMainMenuActions(MainWindow mainWindow) {
-        ensureActions(mainWindow);
+        List<Action> actions = new ArrayList<>();
+        int keypos = 0;
+        for (String layout : LAYOUT_NAMES) {
+            Integer key = keypos < LAYOUT_KEYS.length ? LAYOUT_KEYS[keypos] : null;
+            actions.add(new LoadLayoutAction(mainWindow, layout, key));
+            actions.add(new SaveLayoutAction(mainWindow, layout, key));
+            keypos++;
+        }
+        actions.add(new ResetLayoutAction(mainWindow));
         return actions;
     }
 }
 
 
-class SaveLayoutAction extends MainWindowAction {
+final class SaveLayoutAction extends MainWindowAction {
     private static final long serialVersionUID = -2646217961498111734L;
     private final String layoutName;
 
-    public SaveLayoutAction(MainWindow mainWindow, String name, Integer key) {
+    SaveLayoutAction(MainWindow mainWindow, String name, Integer key) {
         super(mainWindow);
         this.layoutName = name;
         setName("Save as " + name);
@@ -218,11 +167,11 @@ public void actionPerformed(ActionEvent e) {
 }
 
 
-class LoadLayoutAction extends MainWindowAction {
+final class LoadLayoutAction extends MainWindowAction {
     private static final long serialVersionUID = 3378477658914832831L;
     private final String layoutName;
 
-    public LoadLayoutAction(MainWindow mainWindow, String name, Integer key) {
+    LoadLayoutAction(MainWindow mainWindow, String name, Integer key) {
         super(mainWindow);
         this.layoutName = name;
         setName("Load " + name);
@@ -248,14 +197,14 @@ public void actionPerformed(ActionEvent e) {
 }
 
 
-class ResetLayoutAction extends MainWindowAction {
+final class ResetLayoutAction extends MainWindowAction {
     private static final long serialVersionUID = 8772915552504055750L;
 
-    public ResetLayoutAction(MainWindow mainWindow) {
+    ResetLayoutAction(MainWindow mainWindow) {
         super(mainWindow);
         setName("Reset Layout");
         KeyStrokeManager.lookupAndOverride(this);
-        setPriority(-1);
+        setPriority(10);
         setMenuPath("View.Layout");
     }
 

key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java

@@ -26,11 +26,10 @@
  */
 public final class KeYGuiExtensionFacade {
     private static final Set<String> forbiddenPlugins = new HashSet<>();
-    private static List<Extension> extensions = new LinkedList<>();
+    private static List<Extension<?>> extensions = new LinkedList<>();
     // private static Map<Class<?>, List<Object>> extensionCache = new HashMap<>();
 
     // region panel extension
-    // @SuppressWarnings("todo")
     public static Stream<TabPanel> getAllPanels(MainWindow window) {
         return getLeftPanel().stream()
                 .flatMap(it -> it.getPanels(window, window.getMediator()).stream());
@@ -221,6 +220,7 @@ public static List<KeYGuiExtension.Toolbar> getToolbarExtensions() {
      */
     public static List<JToolBar> createToolbars(MainWindow mainWindow) {
         return getToolbarExtensions().stream().map(it -> it.getToolbar(mainWindow))
+                .peek(x -> x.setFloatable(false))
                 .collect(Collectors.toList());
     }
 
@@ -311,7 +311,7 @@ private static <T> boolean isNotForbidden(Class<T> a) {
     }
     // endregion
 
-    public static List<Extension> getExtensions() {
+    public static List<Extension<?>> getExtensions() {
         if (extensions.isEmpty()) {
             loadExtensions();
         }
@@ -374,9 +374,9 @@ public static void installKeyboardShortcuts(KeYMediator mediator, JComponent com
     // region Term tool tip
 
     /**
-     * Retrieves all known implementations of the {@link KeYStatusBarExtension}.
+     * Retrieves all known implementations of the {@link KeYGuiExtension.Tooltip}.
      *
-     * @return all known implementations of the {@link KeYStatusBarExtension}.
+     * @return all known implementations of the {@link KeYGuiExtension.Tooltip}.
      */
     public static List<KeYGuiExtension.Tooltip> getTooltipExtensions() {
         return getExtensionInstances(KeYGuiExtension.Tooltip.class);

keyext.action_history/src/main/java/org/key_project/action_history/ActionHistoryExtension.java → key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java

@@ -1,12 +1,11 @@
-package org.key_project.action_history;
+package de.uka.ilkd.key.gui.plugins.action_history;
 
 import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
 import java.util.WeakHashMap;
-import javax.annotation.Nonnull;
 import javax.swing.*;
 
 import de.uka.ilkd.key.core.KeYMediator;
@@ -15,7 +14,6 @@
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.UserActionListener;
 import de.uka.ilkd.key.gui.actions.useractions.UserAction;
-import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
 import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid;
 import de.uka.ilkd.key.gui.fonticons.IconFontProvider;
 import de.uka.ilkd.key.proof.Proof;
@@ -24,39 +22,27 @@
 
 
 /**
- * Entry point for the Action History extension.
+ * Entry point for the Action History functionality.
  *
  * @author Arne Keller
  */
-@KeYGuiExtension.Info(name = "Action History",
-    description = "GUI extension to undo actions (using a toolbar button)",
-    experimental = false, optional = true, priority = 10000)
-public class ActionHistoryExtension implements KeYGuiExtension,
-        KeYGuiExtension.Startup, KeYGuiExtension.Toolbar, UserActionListener,
+public class ActionHistoryExtension implements UserActionListener,
         ProofDisposedListener, KeYSelectionListener {
     /**
      * Icon for the undo button.
      */
     private static final IconFontProvider UNDO = new IconFontProvider(FontAwesomeSolid.UNDO);
 
-    /**
-     * The KeY mediator.
-     */
-    private KeYMediator mediator;
     /**
      * Tracked user actions, stored separately for each proof.
      */
     private final Map<Proof, List<UserAction>> userActions = new WeakHashMap<>();
 
     /**
-     * The toolbar area for this extension. Contains the dropdown list of performed actions and
-     * the undo button.
-     */
-    private JToolBar extensionToolbar = null;
-    /**
-     * The undo button contained in {@link #extensionToolbar}.
+     * The undo button contained in the main toolbar.
      */
     private UndoHistoryButton undoButton = null;
+    private JButton undoUptoButton = null;
     /**
      * Proofs this extension is monitoring for changes.
      */
@@ -66,23 +52,6 @@
      */
     private Proof currentProof = null;
 
-    @Nonnull
-    @Override
-    public JToolBar getToolbar(MainWindow mainWindow) {
-        if (extensionToolbar == null) {
-            extensionToolbar = new JToolBar();
-            undoButton =
-                new UndoHistoryButton(mainWindow, MainWindow.TOOLBAR_ICON_SIZE, UNDO, "Undo ",
-                    this::undoOneAction, this::undoUptoAction, this::getActions);
-            extensionToolbar.add(undoButton.getAction());
-            JButton undoUptoButton = undoButton.getSelectionButton();
-            undoUptoButton.setToolTipText(
-                "Select an action to undo, including all actions performed afterwards");
-            extensionToolbar.add(undoUptoButton);
-        }
-        return extensionToolbar;
-    }
-
     private List<UserAction> getActions() {
         List<UserAction> actions = userActions.get(currentProof);
         if (actions == null) {
@@ -92,7 +61,7 @@
         for (int i = 0; i < actions.size(); i++) {
             if (!actions.get(i).canUndo()) {
                 actions.remove(i);
                 i--;
             }
         }
         return actions;
@@ -121,12 +90,16 @@
         }
     }
 
-    @Override
-    public void init(MainWindow window, KeYMediator mediator) {
-        this.mediator = mediator;
+    public ActionHistoryExtension(MainWindow window, KeYMediator mediator) {
         mediator.addUserActionListener(this);
         mediator.addKeYSelectionListener(this);
         new StateChangeListener(mediator);
+        undoButton =
+            new UndoHistoryButton(window, MainWindow.TOOLBAR_ICON_SIZE, UNDO, "Undo ",
+                this::undoOneAction, this::undoUptoAction, this::getActions);
+        undoUptoButton = undoButton.getSelectionButton();
+        undoUptoButton.setToolTipText(
+            "Select an action to undo, including all actions performed afterwards");
         undoButton.refreshState();
     }
 
@@ -169,4 +142,12 @@
         registeredProofs.add(p);
         p.addProofDisposedListener(this);
     }
+
+    public JButton getUndoUptoButton() {
+        return undoUptoButton;
+    }
+
+    public UndoHistoryButton getUndoButton() {
+        return undoButton;
+    }
 }

keyext.action_history/src/main/java/org/key_project/action_history/StateChangeListener.java → key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java

@@ -1,4 +1,4 @@
-package org.key_project.action_history;
+package de.uka.ilkd.key.gui.plugins.action_history;
 
 import java.util.List;