From 15514c6c11a0fea51e85701a43934af26bcad0e7 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 9 Jul 2023 14:40:13 +0200 Subject: [PATCH 01/10] Move action history button to main toolbar --- key.ui/build.gradle | 1 - .../java/de/uka/ilkd/key/gui/MainWindow.java | 4 ++ .../ActionHistoryExtension.java | 59 +++++++------------ .../action_history/StateChangeListener.java | 2 +- .../action_history/UndoHistoryButton.java | 4 +- keyext.action_history/build.gradle | 4 -- ...ilkd.key.gui.extension.api.KeYGuiExtension | 1 - settings.gradle | 1 - 8 files changed, 27 insertions(+), 49 deletions(-) rename {keyext.action_history/src/main/java/org/key_project => key.ui/src/main/java/de/uka/ilkd/key/gui/plugins}/action_history/ActionHistoryExtension.java (70%) rename {keyext.action_history/src/main/java/org/key_project => key.ui/src/main/java/de/uka/ilkd/key/gui/plugins}/action_history/StateChangeListener.java (97%) rename {keyext.action_history/src/main/java/org/key_project => key.ui/src/main/java/de/uka/ilkd/key/gui/plugins}/action_history/UndoHistoryButton.java (99%) delete mode 100644 keyext.action_history/build.gradle delete mode 100644 keyext.action_history/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension diff --git a/key.ui/build.gradle b/key.ui/build.gradle index d440f453f81..d6e6467189f 100644 --- a/key.ui/build.gradle +++ b/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") } 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 e3579d07398..ea822deb0e6 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 @@ -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; @@ -647,6 +648,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()); diff --git a/keyext.action_history/src/main/java/org/key_project/action_history/ActionHistoryExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java similarity index 70% rename from keyext.action_history/src/main/java/org/key_project/action_history/ActionHistoryExtension.java rename to key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java index eb37d16b26a..c285aa563bb 100644 --- a/keyext.action_history/src/main/java/org/key_project/action_history/ActionHistoryExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java @@ -1,4 +1,4 @@ -package org.key_project.action_history; +package de.uka.ilkd.key.gui.plugins.action_history; import java.util.ArrayList; import java.util.HashSet; @@ -6,7 +6,6 @@ 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> 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 @@ public class ActionHistoryExtension implements KeYGuiExtension, */ 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 getActions() { List actions = userActions.get(currentProof); if (actions == null) { @@ -121,12 +90,16 @@ private void undoUptoAction(UserAction userAction) { } } - @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 @@ public void selectedProofChanged(KeYSelectionEvent e) { registeredProofs.add(p); p.addProofDisposedListener(this); } + + public JButton getUndoUptoButton() { + return undoUptoButton; + } + + public UndoHistoryButton getUndoButton() { + return undoButton; + } } diff --git a/keyext.action_history/src/main/java/org/key_project/action_history/StateChangeListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java similarity index 97% rename from keyext.action_history/src/main/java/org/key_project/action_history/StateChangeListener.java rename to key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java index 9f6bd06861c..2978737e68b 100644 --- a/keyext.action_history/src/main/java/org/key_project/action_history/StateChangeListener.java +++ b/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; diff --git a/keyext.action_history/src/main/java/org/key_project/action_history/UndoHistoryButton.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/UndoHistoryButton.java similarity index 99% rename from keyext.action_history/src/main/java/org/key_project/action_history/UndoHistoryButton.java rename to key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/UndoHistoryButton.java index 06c4ee783a7..4c1174095da 100644 --- a/keyext.action_history/src/main/java/org/key_project/action_history/UndoHistoryButton.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/UndoHistoryButton.java @@ -1,4 +1,4 @@ -package org.key_project.action_history; +package de.uka.ilkd.key.gui.plugins.action_history; import java.awt.event.*; import java.util.*; @@ -171,7 +171,7 @@ public void actionPerformed(ActionEvent e) { * * @return the action */ - protected MainWindowAction getAction() { + public MainWindowAction getAction() { return action; } diff --git a/keyext.action_history/build.gradle b/keyext.action_history/build.gradle deleted file mode 100644 index c448ade9d8c..00000000000 --- a/keyext.action_history/build.gradle +++ /dev/null @@ -1,4 +0,0 @@ -dependencies { - implementation project(":key.core") - implementation project(":key.ui") -} \ No newline at end of file diff --git a/keyext.action_history/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.action_history/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension deleted file mode 100644 index 17e6acd25f9..00000000000 --- a/keyext.action_history/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ /dev/null @@ -1 +0,0 @@ -org.key_project.action_history.ActionHistoryExtension \ No newline at end of file diff --git a/settings.gradle b/settings.gradle index f0e5c4d97ac..12b3d123ece 100644 --- a/settings.gradle +++ b/settings.gradle @@ -11,6 +11,5 @@ include "key.core.example" include "key.core.symbolic_execution.example" include 'recoder' include 'keyext.ui.testgen' -include 'keyext.action_history' include 'keyext.exploration' include 'keyext.slicing' From bac3220788dbc7c3c607615f7e9c1a2b3ae4d740 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 10 Jul 2023 21:35:33 +0200 Subject: [PATCH 02/10] Make exploration extension experimental --- .../java/org/key_project/exploration/ExplorationExtension.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java b/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java index 981f4f9e591..84fe0486caf 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java @@ -39,7 +39,7 @@ */ @KeYGuiExtension.Info(name = "Exploration", description = "Author: Sarah Grebing , Alexander Weigl ", - experimental = false, optional = true, priority = 10000) + experimental = true, optional = true, priority = 10000) public class ExplorationExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu, KeYGuiExtension.Startup, KeYGuiExtension.Toolbar, KeYGuiExtension.MainMenu, KeYGuiExtension.LeftPanel, KeYGuiExtension.StatusLine, ProofDisposedListener { From 07addf25c44f82148ee4b2302d87da0b936beb15 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 10 Jul 2023 21:44:53 +0200 Subject: [PATCH 03/10] Move layout controls to menu --- .../ilkd/key/gui/docking/DockingLayout.java | 169 ++++++++---------- .../gui/extension/api/KeYGuiExtension.java | 19 +- .../extension/impl/KeYGuiExtensionFacade.java | 32 ++-- 3 files changed, 104 insertions(+), 116 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 226916fb40b..3ab88dd471c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -8,6 +8,7 @@ import java.io.IOException; import java.util.*; import java.util.List; +import javax.annotation.Nonnull; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; @@ -37,16 +38,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 }; - private final List actions = new LinkedList<>(); + private final ButtonGroup layouts = new ButtonGroup(); private MainWindow window; private void installIcons(MainWindow mw) { @@ -90,18 +90,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; @@ -124,7 +112,7 @@ public void shutDown(EventObject e) { try { window.getDockControl().writeXML(LAYOUT_FILE); } catch (IOException ex) { - LOGGER.warn("Failed to save layouts", ex); + LOGGER.warn("Failed to save layouts ", ex); } } }); @@ -139,111 +127,101 @@ private void setLayout(String layout) { } } + @Nonnull @Override - public JToolBar getToolbar(MainWindow mainWindow) { - JToolBar toolBar = new JToolBar("Docking Layout"); - JComboBox comboLayouts = new JComboBox<>(); + public List getMainMenuItems(@Nonnull MainWindow mainWindow) { + List items = new ArrayList<>(); - class SaveAction extends MainWindowAction { - private static final long serialVersionUID = -2688272657370615595L; + final class ActivateLayoutAction extends MainWindowAction { + private final String layout; - protected SaveAction(MainWindow mainWindow) { + private ActivateLayoutAction(MainWindow mainWindow, String layout) { super(mainWindow); - setName("Save Layout"); + this.layout = layout; + setName(layout); + setMenuPath("View.Layout"); } @Override public void actionPerformed(ActionEvent e) { - String name = Objects.requireNonNull(comboLayouts.getSelectedItem()).toString(); - mainWindow.getDockControl().save(name); + setLayout(layout); + layouts.getElements().asIterator().forEachRemaining( + button -> button.getModel().setSelected(button.getText().contains(layout))); } } - 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); + JRadioButtonMenuItem button = new JRadioButtonMenuItem(s); + if (s.equals("Default")) { + button.getModel().setSelected(true); + } else { + button.getModel().setSelected(false); + } + layouts.add(button); + button.setAction(new ActivateLayoutAction(mainWindow, s)); + items.add(button); } - toolBar.add(comboLayouts); - toolBar.add(new LoadAction(mainWindow)); - toolBar.add(new SaveAction(mainWindow)); - toolBar.addSeparator(); - toolBar.add(new ResetLayoutAction(mainWindow)); - return toolBar; + return items; } @Override public List getMainMenuActions(MainWindow mainWindow) { - ensureActions(mainWindow); - return actions; - } -} + List actions = new ArrayList<>(); + final class SaveAction extends MainWindowAction { + private static final long serialVersionUID = -2688272657370615595L; -class SaveLayoutAction extends MainWindowAction { - private static final long serialVersionUID = -2646217961498111734L; - private final String layoutName; + private SaveAction(MainWindow mainWindow) { + super(mainWindow); + setName("Save Layout"); + setMenuPath("View.Layout"); + } - public SaveLayoutAction(MainWindow mainWindow, String name, Integer key) { - super(mainWindow); - this.layoutName = name; - setName("Save as " + name); - setIcon(IconFactory.saveFile(MainWindow.TOOLBAR_ICON_SIZE)); - setMenuPath("View.Layout.Save"); - if (key != null) { - setAcceleratorKey(KeyStroke.getKeyStroke(key, - InputEvent.CTRL_DOWN_MASK | InputEvent.SHIFT_DOWN_MASK)); + @Override + public void actionPerformed(ActionEvent e) { + String layout = null; + var iter = layouts.getElements().asIterator(); + while (iter.hasNext()) { + var b = (JRadioButtonMenuItem) iter.next(); + if (b.getModel().isSelected()) { + layout = b.getText(); + System.out.println("saving in " + layout); + break; + } + } + mainWindow.getDockControl().save(layout); + } } - KeyStrokeManager.lookupAndOverride(this, getClass().getName() + "$" + layoutName); - } - - @Override - public void actionPerformed(ActionEvent e) { - mainWindow.getDockControl().save(layoutName); - mainWindow.setStatusLine("Save layout as " + layoutName); - } -} + final class LoadAction extends MainWindowAction { + private static final long serialVersionUID = 3130337190207622893L; -class LoadLayoutAction extends MainWindowAction { - private static final long serialVersionUID = 3378477658914832831L; - private final String layoutName; + private LoadAction(MainWindow mainWindow) { + super(mainWindow); + setName("Load Layout"); + setMenuPath("View.Layout"); + } - public LoadLayoutAction(MainWindow mainWindow, String name, Integer key) { - super(mainWindow); - this.layoutName = name; - setName("Load " + name); - setIcon(IconFactory.openKeYFile(MainWindow.TOOLBAR_ICON_SIZE)); - if (key != null) { - setAcceleratorKey(KeyStroke.getKeyStroke(key, InputEvent.CTRL_DOWN_MASK)); + @Override + public void actionPerformed(ActionEvent e) { + String layout = null; + var iter = layouts.getElements().asIterator(); + while (iter.hasNext()) { + var b = (JRadioButtonMenuItem) iter.next(); + if (b.getModel().isSelected()) { + layout = b.getText(); + break; + } + } + setLayout(layout); + } } - KeyStrokeManager.lookupAndOverride(this, getClass().getName() + "$" + layoutName); - setMenuPath("View.Layout.Load"); - } - @Override - public void actionPerformed(ActionEvent e) { - boolean defaultLayoutDefined = - Arrays.asList(mainWindow.getDockControl().layouts()).contains(layoutName); - if (defaultLayoutDefined) { - mainWindow.getDockControl().load(layoutName); - mainWindow.setStatusLine("Layout " + layoutName + " loaded"); - } else { - mainWindow.setStatusLine("Layout " + layoutName + " could not be found."); - } + actions.add(new LoadAction(mainWindow)); + actions.add(new SaveAction(mainWindow)); + actions.add(new ResetLayoutAction(mainWindow)); + + return actions; } } @@ -255,7 +233,6 @@ public ResetLayoutAction(MainWindow mainWindow) { super(mainWindow); setName("Reset Layout"); KeyStrokeManager.lookupAndOverride(this); - setPriority(-1); setMenuPath("View.Layout"); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index 19c35579179..50316975e9e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java @@ -3,12 +3,10 @@ import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.util.Collection; +import java.util.Collections; import java.util.List; import javax.annotation.Nonnull; -import javax.swing.Action; -import javax.swing.JComponent; -import javax.swing.JMenu; -import javax.swing.JToolBar; +import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.GoalList; @@ -100,6 +98,19 @@ interface MainMenu { */ @Nonnull List getMainMenuActions(@Nonnull MainWindow mainWindow); + + /** + * A list of menu items which should be added to the main menu. + * These will be added before the actions returned by + * {@link #getMainMenuActions(MainWindow)} are added. + * + * @param mainWindow the main window + * @return list of menu items + */ + @Nonnull + default List getMainMenuItems(@Nonnull MainWindow mainWindow) { + return Collections.emptyList(); + } } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 761b50171eb..69d76e7d61c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -25,11 +25,10 @@ */ public final class KeYGuiExtensionFacade { private static final Set forbiddenPlugins = new HashSet<>(); - private static List extensions = new LinkedList<>(); + private static List> extensions = new LinkedList<>(); // private static Map, List> extensionCache = new HashMap<>(); // region panel extension - // @SuppressWarnings("todo") public static Stream getAllPanels(MainWindow window) { return getLeftPanel().stream() .flatMap(it -> it.getPanels(window, window.getMediator()).stream()); @@ -68,11 +67,12 @@ public static Stream getMainMenuActions(MainWindow mainWindow) { /** * Adds all registered and activated {@link KeYGuiExtension.MainMenu} to the given menuBar. - * - * @return a menu */ public static void addExtensionsToMainMenu(MainWindow mainWindow, JMenuBar menuBar) { JMenu menu = new JMenu("Extensions"); + KeYGuiExtensionFacade.getMainMenuExtensions().stream() + .flatMap(it -> it.getMainMenuItems(mainWindow).stream()) + .forEach(it -> sortItemIntoMenu(it, menuBar, menu)); getMainMenuActions(mainWindow).forEach(it -> sortActionIntoMenu(it, menuBar, menu)); if (menu.getMenuComponents().length > 0) { @@ -81,14 +81,6 @@ public static void addExtensionsToMainMenu(MainWindow mainWindow, JMenuBar menuB } - /* - * public static Optional getMainMenuExtensions(String name) { - * Spliterator iter = - * ServiceLoader.load(KeYGuiExtension.MainMenu.class).spliterator(); return - * StreamSupport.stream(iter, false) .flatMap(it -> it.getMainMenuActions(mainWindow).stream()) - * .filter(Objects::nonNull) .filter(it -> it.getValue(Action.NAME).equals(name)) .findAny(); } - */ - // region Menu Helper private static void sortActionsIntoMenu(List actions, JMenuBar menuBar) { actions.forEach(act -> sortActionIntoMenu(act, menuBar, new JMenu())); @@ -105,6 +97,10 @@ private static Iterator getMenuPath(Action act) { return Pattern.compile(Pattern.quote(".")).splitAsStream(spath).iterator(); } + private static Iterator getMenuPath(JMenuItem item) { + return getMenuPath(item.getAction()); + } + private static void sortActionIntoMenu(Action act, JMenu menu) { Iterator mpath = getMenuPath(act); JMenu a = findMenu(menu, mpath); @@ -135,6 +131,12 @@ private static void sortActionIntoMenu(Action act, JPopupMenu menu) { } } + private static void sortItemIntoMenu(JMenuItem item, JMenuBar menuBar, JMenu defaultMenu) { + Iterator mpath = getMenuPath(item); + JMenu a = findMenu(menuBar, mpath, defaultMenu); + a.add(item); + } + private static void sortActionIntoMenu(Action act, JMenuBar menuBar, JMenu defaultMenu) { Iterator mpath = getMenuPath(act); JMenu a = findMenu(menuBar, mpath, defaultMenu); @@ -304,7 +306,7 @@ private static boolean isNotForbidden(Class a) { } // endregion - public static List getExtensions() { + public static List> getExtensions() { if (extensions.isEmpty()) { loadExtensions(); } @@ -367,9 +369,7 @@ public static void installKeyboardShortcuts(KeYMediator mediator, JComponent com // region Term tool tip /** - * Retrieves all known implementations of the {@link KeYStatusBarExtension}. - * - * @return all known implementations of the {@link KeYStatusBarExtension}. + * @return all known implementations of the {@link KeYGuiExtension.Tooltip} */ public static List getTooltipExtensions() { return getExtensionInstances(KeYGuiExtension.Tooltip.class); From 3a9bf5970387808fcfd8445c73f4a9ba0995f186 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 10 Jul 2023 21:49:24 +0200 Subject: [PATCH 04/10] Fix extension panels not showing up sometimes --- .../main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 3ab88dd471c..28a6405bfdb 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -123,8 +123,8 @@ private void setLayout(String layout) { boolean defaultLayoutDefined = Arrays.asList(globalPort.layouts()).contains(layout); if (defaultLayoutDefined) { globalPort.load(layout); - DockingHelper.restoreMissingPanels(window); } + DockingHelper.restoreMissingPanels(window); } @Nonnull From 3c91c4f55986949317e055b596c7ef51a57adde3 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 11 Jul 2023 07:39:30 +0200 Subject: [PATCH 05/10] Disable rearrangement of toolbar --- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 5 +++-- .../ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java | 1 + 2 files changed, 4 insertions(+), 2 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 04375ab5815..ae6f364eb25 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 @@ -622,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); @@ -635,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()); @@ -660,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); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 4a207452aca..283a41c8499 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -223,6 +223,7 @@ public static List getToolbarExtensions() { */ public static List createToolbars(MainWindow mainWindow) { return getToolbarExtensions().stream().map(it -> it.getToolbar(mainWindow)) + .peek(x -> x.setFloatable(false)) .collect(Collectors.toList()); } From e15bc0e7d4378d7cbc55c1c92556ba5d4c821d02 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 14 Jul 2023 09:46:11 +0200 Subject: [PATCH 06/10] Revert "Move layout controls to menu" This reverts commit 07addf25c44f82148ee4b2302d87da0b936beb15. --- .../uka/ilkd/key/gui/actions/KeyAction.java | 5 + .../ilkd/key/gui/docking/DockingLayout.java | 123 ++---------------- .../gui/extension/api/KeYGuiExtension.java | 19 +-- .../extension/impl/KeYGuiExtensionFacade.java | 27 ++-- 4 files changed, 34 insertions(+), 140 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java index 4cd5056ea63..9f38214082f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java +++ b/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); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 33af200fbf2..63637b48668 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -8,7 +8,6 @@ import java.io.IOException; import java.util.*; import java.util.List; -import javax.annotation.Nonnull; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; @@ -46,8 +45,6 @@ public final class DockingLayout implements KeYGuiExtension, KeYGuiExtension.Sta 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 }; - private final List actions = new LinkedList<>(); - private final ButtonGroup layouts = new ButtonGroup(); private MainWindow window; private void installIcons(MainWindow mw) { @@ -91,18 +88,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; @@ -125,7 +110,7 @@ public void shutDown(EventObject e) { try { window.getDockControl().writeXML(LAYOUT_FILE); } catch (IOException ex) { - LOGGER.warn("Failed to save layouts ", ex); + LOGGER.warn("Failed to save layouts", ex); } } }); @@ -140,102 +125,17 @@ private void setLayout(String layout) { DockingHelper.restoreMissingPanels(window); } - @Nonnull - @Override - public List getMainMenuItems(@Nonnull MainWindow mainWindow) { - List items = new ArrayList<>(); - - final class ActivateLayoutAction extends MainWindowAction { - private final String layout; - - private ActivateLayoutAction(MainWindow mainWindow, String layout) { - super(mainWindow); - this.layout = layout; - setName(layout); - setMenuPath("View.Layout"); - } - - @Override - public void actionPerformed(ActionEvent e) { - setLayout(layout); - layouts.getElements().asIterator().forEachRemaining( - button -> button.getModel().setSelected(button.getText().contains(layout))); - } - } - - for (String s : LAYOUT_NAMES) { - JRadioButtonMenuItem button = new JRadioButtonMenuItem(s); - if (s.equals("Default")) { - button.getModel().setSelected(true); - } else { - button.getModel().setSelected(false); - } - layouts.add(button); - button.setAction(new ActivateLayoutAction(mainWindow, s)); - items.add(button); - } - return items; - } - @Override public List getMainMenuActions(MainWindow mainWindow) { List actions = new ArrayList<>(); - - final class SaveAction extends MainWindowAction { - private static final long serialVersionUID = -2688272657370615595L; - - private SaveAction(MainWindow mainWindow) { - super(mainWindow); - setName("Save Layout"); - setMenuPath("View.Layout"); - } - - @Override - public void actionPerformed(ActionEvent e) { - String layout = null; - var iter = layouts.getElements().asIterator(); - while (iter.hasNext()) { - var b = (JRadioButtonMenuItem) iter.next(); - if (b.getModel().isSelected()) { - layout = b.getText(); - System.out.println("saving in " + layout); - break; - } - } - mainWindow.getDockControl().save(layout); - } + 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++; } - - final class LoadAction extends MainWindowAction { - private static final long serialVersionUID = 3130337190207622893L; - - private LoadAction(MainWindow mainWindow) { - super(mainWindow); - setName("Load Layout"); - setMenuPath("View.Layout"); - } - - @Override - public void actionPerformed(ActionEvent e) { - String layout = null; - var iter = layouts.getElements().asIterator(); - while (iter.hasNext()) { - var b = (JRadioButtonMenuItem) iter.next(); - if (b.getModel().isSelected()) { - layout = b.getText(); - break; - } - } - setLayout(layout); - } - } - - actions.add(new LoadAction(mainWindow)); - actions.add(new SaveAction(mainWindow)); actions.add(new ResetLayoutAction(mainWindow)); - - ensureActions(mainWindow); - return actions; } } @@ -245,7 +145,7 @@ 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); @@ -270,7 +170,7 @@ 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); @@ -296,13 +196,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(10); setMenuPath("View.Layout"); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index 50316975e9e..19c35579179 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java @@ -3,10 +3,12 @@ import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.util.Collection; -import java.util.Collections; import java.util.List; import javax.annotation.Nonnull; -import javax.swing.*; +import javax.swing.Action; +import javax.swing.JComponent; +import javax.swing.JMenu; +import javax.swing.JToolBar; import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.GoalList; @@ -98,19 +100,6 @@ interface MainMenu { */ @Nonnull List getMainMenuActions(@Nonnull MainWindow mainWindow); - - /** - * A list of menu items which should be added to the main menu. - * These will be added before the actions returned by - * {@link #getMainMenuActions(MainWindow)} are added. - * - * @param mainWindow the main window - * @return list of menu items - */ - @Nonnull - default List getMainMenuItems(@Nonnull MainWindow mainWindow) { - return Collections.emptyList(); - } } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 283a41c8499..5aae827c2c0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -68,12 +68,11 @@ public static Stream getMainMenuActions(MainWindow mainWindow) { /** * Adds all registered and activated {@link KeYGuiExtension.MainMenu} to the given menuBar. + * + * @return a menu */ public static void addExtensionsToMainMenu(MainWindow mainWindow, JMenuBar menuBar) { JMenu menu = new JMenu("Extensions"); - KeYGuiExtensionFacade.getMainMenuExtensions().stream() - .flatMap(it -> it.getMainMenuItems(mainWindow).stream()) - .forEach(it -> sortItemIntoMenu(it, menuBar, menu)); getMainMenuActions(mainWindow).forEach(it -> sortActionIntoMenu(it, menuBar, menu)); if (menu.getMenuComponents().length > 0) { @@ -82,6 +81,14 @@ public static void addExtensionsToMainMenu(MainWindow mainWindow, JMenuBar menuB } + /* + * public static Optional getMainMenuExtensions(String name) { + * Spliterator iter = + * ServiceLoader.load(KeYGuiExtension.MainMenu.class).spliterator(); return + * StreamSupport.stream(iter, false) .flatMap(it -> it.getMainMenuActions(mainWindow).stream()) + * .filter(Objects::nonNull) .filter(it -> it.getValue(Action.NAME).equals(name)) .findAny(); } + */ + // region Menu Helper private static void sortActionsIntoMenu(List actions, JMenuBar menuBar) { actions.forEach(act -> sortActionIntoMenu(act, menuBar, new JMenu())); @@ -98,10 +105,6 @@ private static Iterator getMenuPath(Action act) { return Pattern.compile(Pattern.quote(".")).splitAsStream(spath).iterator(); } - private static Iterator getMenuPath(JMenuItem item) { - return getMenuPath(item.getAction()); - } - private static void sortActionIntoMenu(Action act, JMenu menu) { Iterator mpath = getMenuPath(act); JMenu a = findMenu(menu, mpath); @@ -132,12 +135,6 @@ private static void sortActionIntoMenu(Action act, JPopupMenu menu) { } } - private static void sortItemIntoMenu(JMenuItem item, JMenuBar menuBar, JMenu defaultMenu) { - Iterator mpath = getMenuPath(item); - JMenu a = findMenu(menuBar, mpath, defaultMenu); - a.add(item); - } - private static void sortActionIntoMenu(Action act, JMenuBar menuBar, JMenu defaultMenu) { Iterator mpath = getMenuPath(act); JMenu a = findMenu(menuBar, mpath, defaultMenu); @@ -377,7 +374,9 @@ public static void installKeyboardShortcuts(KeYMediator mediator, JComponent com // region Term tool tip /** - * @return all known implementations of the {@link KeYGuiExtension.Tooltip} + * Retrieves all known implementations of the {@link KeYGuiExtension.Tooltip}. + * + * @return all known implementations of the {@link KeYGuiExtension.Tooltip}. */ public static List getTooltipExtensions() { return getExtensionInstances(KeYGuiExtension.Tooltip.class); From cebf0c5c48bb0822310b4f690c41cfae4abec1ea Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 14 Jul 2023 10:07:21 +0200 Subject: [PATCH 07/10] Add shortcut key for last layout action --- .../main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 63637b48668..7515e39c547 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -43,7 +43,8 @@ public final class DockingLayout implements KeYGuiExtension, KeYGuiExtension.Sta 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 MainWindow window; From 1562cdd771a1962ec74053c1ff915c7388839d5b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 15 Jul 2023 15:45:33 +0200 Subject: [PATCH 08/10] All layout actions in one sub-menu --- .../main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 7515e39c547..a392fa9614b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -151,7 +151,7 @@ final class SaveLayoutAction extends MainWindowAction { this.layoutName = name; setName("Save as " + name); setIcon(IconFactory.saveFile(MainWindow.TOOLBAR_ICON_SIZE)); - setMenuPath("View.Layout.Save"); + setMenuPath("View.Layout"); if (key != null) { setAcceleratorKey(KeyStroke.getKeyStroke(key, InputEvent.CTRL_DOWN_MASK | InputEvent.SHIFT_DOWN_MASK)); @@ -180,7 +180,7 @@ final class LoadLayoutAction extends MainWindowAction { setAcceleratorKey(KeyStroke.getKeyStroke(key, InputEvent.CTRL_DOWN_MASK)); } KeyStrokeManager.lookupAndOverride(this, getClass().getName() + "$" + layoutName); - setMenuPath("View.Layout.Load"); + setMenuPath("View.Layout"); } @Override From 5544075cc9b845f498d807961cad303dcc22125d Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 15 Jul 2023 18:13:50 +0200 Subject: [PATCH 09/10] Harmonize action and status bar labels --- .../ilkd/key/gui/docking/DockingLayout.java | 23 ++++++++++++------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index a392fa9614b..f89ec376e0d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -8,6 +8,7 @@ import java.io.IOException; import java.util.*; import java.util.List; +import javax.annotation.Nonnull; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; @@ -40,10 +41,10 @@ public final class DockingLayout implements KeYGuiExtension, KeYGuiExtension.Sta 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 = + private static final float SIZE_ICON_DOCK = 12f; + private static final File LAYOUT_FILE = new File(PathConfig.getKeyConfigDir(), "layout.xml"); + private static final String[] LAYOUT_NAMES = new String[] { "Default", "Slot 1", "Slot 2" }; + private static final int[] LAYOUT_KEYS = new int[] { KeyEvent.VK_F10, KeyEvent.VK_F11, KeyEvent.VK_F12 }; private MainWindow window; @@ -126,13 +127,19 @@ private void setLayout(String layout) { DockingHelper.restoreMissingPanels(window); } + @Nonnull @Override - public List getMainMenuActions(MainWindow mainWindow) { + public List getMainMenuActions(@Nonnull MainWindow mainWindow) { List 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)); + keypos++; + } + keypos = 0; + for (String layout : LAYOUT_NAMES) { + Integer key = keypos < LAYOUT_KEYS.length ? LAYOUT_KEYS[keypos] : null; actions.add(new SaveLayoutAction(mainWindow, layout, key)); keypos++; } @@ -149,7 +156,7 @@ final class SaveLayoutAction extends MainWindowAction { SaveLayoutAction(MainWindow mainWindow, String name, Integer key) { super(mainWindow); this.layoutName = name; - setName("Save as " + name); + setName("Save " + name); setIcon(IconFactory.saveFile(MainWindow.TOOLBAR_ICON_SIZE)); setMenuPath("View.Layout"); if (key != null) { @@ -162,7 +169,7 @@ final class SaveLayoutAction extends MainWindowAction { @Override public void actionPerformed(ActionEvent e) { mainWindow.getDockControl().save(layoutName); - mainWindow.setStatusLine("Save layout as " + layoutName); + mainWindow.setStatusLine("Layout saved to " + layoutName); } } @@ -189,7 +196,7 @@ public void actionPerformed(ActionEvent e) { Arrays.asList(mainWindow.getDockControl().layouts()).contains(layoutName); if (defaultLayoutDefined) { mainWindow.getDockControl().load(layoutName); - mainWindow.setStatusLine("Layout " + layoutName + " loaded"); + mainWindow.setStatusLine("Layout loaded from " + layoutName); } else { mainWindow.setStatusLine("Layout " + layoutName + " could not be found."); } From 85357af588dc0ca9bfa7326daeab355146f6ffd1 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sat, 15 Jul 2023 18:24:38 +0200 Subject: [PATCH 10/10] Remove dead code --- .../key/gui/extension/impl/KeYGuiExtensionFacade.java | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 5aae827c2c0..f5784b3cb6d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -81,18 +81,7 @@ public static void addExtensionsToMainMenu(MainWindow mainWindow, JMenuBar menuB } - /* - * public static Optional getMainMenuExtensions(String name) { - * Spliterator iter = - * ServiceLoader.load(KeYGuiExtension.MainMenu.class).spliterator(); return - * StreamSupport.stream(iter, false) .flatMap(it -> it.getMainMenuActions(mainWindow).stream()) - * .filter(Objects::nonNull) .filter(it -> it.getValue(Action.NAME).equals(name)) .findAny(); } - */ - // region Menu Helper - private static void sortActionsIntoMenu(List actions, JMenuBar menuBar) { - actions.forEach(act -> sortActionIntoMenu(act, menuBar, new JMenu())); - } private static Iterator getMenuPath(Action act) { Object path = act.getValue(KeyAction.PATH);