Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Reduce clutter in toolbar #3198

Merged
merged 12 commits into from
Jul 15, 2023
Merged

Reduce clutter in toolbar #3198

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
15514c6
Move action history button to main toolbar
FliegendeWurst Jul 9, 2023
bac3220
Make exploration extension experimental
FliegendeWurst Jul 10, 2023
07addf2
Move layout controls to menu
FliegendeWurst Jul 10, 2023
3a9bf59
Fix extension panels not showing up sometimes
FliegendeWurst Jul 10, 2023
7996258
Merge remote-tracking branch 'origin/main' into toolbarCleanup
FliegendeWurst Jul 10, 2023
3c91c4f
Disable rearrangement of toolbar
FliegendeWurst Jul 11, 2023
e15bc0e
Revert "Move layout controls to menu"
FliegendeWurst Jul 14, 2023
cebf0c5
Add shortcut key for last layout action
FliegendeWurst Jul 14, 2023
175c05c
Merge remote-tracking branch 'origin/main' into toolbarCleanup
FliegendeWurst Jul 14, 2023
1562cdd
All layout actions in one sub-menu
FliegendeWurst Jul 15, 2023
5544075
Harmonize action and status bar labels
FliegendeWurst Jul 15, 2023
85357af
Remove dead code
FliegendeWurst Jul 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down
126 changes: 14 additions & 112 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -44,10 +43,9 @@ 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 final List<Action> actions = new LinkedList<>();
private final ButtonGroup layouts = new ButtonGroup();
private MainWindow window;

private void installIcons(MainWindow mw) {
Expand Down Expand Up @@ -91,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;
Expand All @@ -125,7 +111,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);
}
}
});
Expand All @@ -140,102 +126,17 @@ private void setLayout(String layout) {
DockingHelper.restoreMissingPanels(window);
}

@Nonnull
@Override
public List<JMenuItem> getMainMenuItems(@Nonnull MainWindow mainWindow) {
List<JMenuItem> 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<Action> getMainMenuActions(MainWindow mainWindow) {
List<Action> 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++;
FliegendeWurst marked this conversation as resolved.
Show resolved Hide resolved
}

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;
}
}
Expand All @@ -245,7 +146,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);
FliegendeWurst marked this conversation as resolved.
Show resolved Hide resolved
Expand All @@ -270,7 +171,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);
Expand All @@ -296,13 +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(10);
setMenuPath("View.Layout");
}

Expand Down
19 changes: 4 additions & 15 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -98,19 +100,6 @@ interface MainMenu {
*/
@Nonnull
List<Action> 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<JMenuItem> getMainMenuItems(@Nonnull MainWindow mainWindow) {
return Collections.emptyList();
}
}

/**
Expand Down
27 changes: 13 additions & 14 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,12 +68,11 @@ public static Stream<Action> 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) {
Expand All @@ -82,6 +81,14 @@ public static void addExtensionsToMainMenu(MainWindow mainWindow, JMenuBar menuB

}

/*
* public static Optional<Action> getMainMenuExtensions(String name) {
* Spliterator<KeYGuiExtension.MainMenu> 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(); }
*/

FliegendeWurst marked this conversation as resolved.
Show resolved Hide resolved
// region Menu Helper
private static void sortActionsIntoMenu(List<Action> actions, JMenuBar menuBar) {
actions.forEach(act -> sortActionIntoMenu(act, menuBar, new JMenu()));
Expand All @@ -98,10 +105,6 @@ private static Iterator<String> getMenuPath(Action act) {
return Pattern.compile(Pattern.quote(".")).splitAsStream(spath).iterator();
}

private static Iterator<String> getMenuPath(JMenuItem item) {
return getMenuPath(item.getAction());
}

private static void sortActionIntoMenu(Action act, JMenu menu) {
Iterator<String> mpath = getMenuPath(act);
JMenu a = findMenu(menu, mpath);
Expand Down Expand Up @@ -132,12 +135,6 @@ private static void sortActionIntoMenu(Action act, JPopupMenu menu) {
}
}

private static void sortItemIntoMenu(JMenuItem item, JMenuBar menuBar, JMenu defaultMenu) {
Iterator<String> mpath = getMenuPath(item);
JMenu a = findMenu(menuBar, mpath, defaultMenu);
a.add(item);
}

private static void sortActionIntoMenu(Action act, JMenuBar menuBar, JMenu defaultMenu) {
Iterator<String> mpath = getMenuPath(act);
JMenu a = findMenu(menuBar, mpath, defaultMenu);
Expand Down Expand Up @@ -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<KeYGuiExtension.Tooltip> getTooltipExtensions() {
return getExtensionInstances(KeYGuiExtension.Tooltip.class);
Expand Down
Loading