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 b615f5fa941..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 @@ -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); 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 226916fb40b..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; @@ -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"); + 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 }; - 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 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; @@ -135,74 +123,42 @@ 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 @Override - public JToolBar getToolbar(MainWindow mainWindow) { - JToolBar toolBar = new JToolBar("Docking Layout"); - JComboBox 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()); - } + 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++; } - - toolBar.add(new JLabel("Layouts: ")); - for (String s : LAYOUT_NAMES) { - comboLayouts.addItem(s); + 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++; } - toolBar.add(comboLayouts); - toolBar.add(new LoadAction(mainWindow)); - toolBar.add(new SaveAction(mainWindow)); - toolBar.addSeparator(); - toolBar.add(new ResetLayoutAction(mainWindow)); - return toolBar; - } - - @Override - public List getMainMenuActions(MainWindow mainWindow) { - ensureActions(mainWindow); + 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); + setName("Save " + 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)); @@ -213,16 +169,16 @@ public SaveLayoutAction(MainWindow mainWindow, String name, Integer key) { @Override public void actionPerformed(ActionEvent e) { mainWindow.getDockControl().save(layoutName); - mainWindow.setStatusLine("Save layout as " + layoutName); + mainWindow.setStatusLine("Layout saved to " + layoutName); } } -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); @@ -231,7 +187,7 @@ public LoadLayoutAction(MainWindow mainWindow, String name, Integer key) { setAcceleratorKey(KeyStroke.getKeyStroke(key, InputEvent.CTRL_DOWN_MASK)); } KeyStrokeManager.lookupAndOverride(this, getClass().getName() + "$" + layoutName); - setMenuPath("View.Layout.Load"); + setMenuPath("View.Layout"); } @Override @@ -240,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."); } @@ -248,14 +204,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"); } 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 25fc032f258..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 @@ -26,11 +26,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()); @@ -82,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); @@ -221,6 +209,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()); } @@ -311,7 +300,7 @@ private static boolean isNotForbidden(Class a) { } // endregion - public static List getExtensions() { + public static List> getExtensions() { if (extensions.isEmpty()) { loadExtensions(); } @@ -374,9 +363,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 getTooltipExtensions() { return getExtensionInstances(KeYGuiExtension.Tooltip.class); 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/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 { 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'