Skip to content

Commit

Permalink
Reduce clutter in toolbar (#3198)
Browse files Browse the repository at this point in the history 
![image](https://github.com/KeYProject/key/assets/12560461/47284086-31cd-453d-8eb0-e5218b68b402)
View menu:

![image](https://github.com/KeYProject/key/assets/12560461/db0b5559-6f56-41da-90ce-716c337bf106)

This reduces clutter in the main toolbar by:
- moving the action history next to the other undo buttons
- moving the layout controls to a menu (View -> Layout)
- marking the exploration extension as experimental (as documented)
- disabling the functionality to reorder toolbars (only ever used by
accident)

As a bonus, the bug that extension panels sometimes fail to show up
should also be fixed.
  • Loading branch information
@WolframPfeifer
WolframPfeifer authored Jul 15, 2023
2 parents f798501 + 85357af commit c482269
Show file tree
Hide file tree
Showing 12 changed files with 75 additions and 146 deletions.
1 change: 0 additions & 1 deletion key.ui/build.gradle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
}
Expand Down
9 changes: 7 additions & 2 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand All @@ -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());
Expand All @@ -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());
Expand All @@ -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);
Expand Down
5 changes: 5 additions & 0 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java
View file
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
112 changes: 34 additions & 78 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<Action> actions = new LinkedList<>();
private MainWindow window;

private void installIcons(MainWindow mw) {
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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<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());
}
public List<Action> getMainMenuActions(@Nonnull MainWindow 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));
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<Action> 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));
Expand All @@ -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);
Expand All @@ -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
Expand All @@ -240,22 +196,22 @@ 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.");
}
}
}


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");
}

Expand Down
21 changes: 5 additions & 16 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down Expand Up @@ -82,18 +81,7 @@ 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(); }
*/

// region Menu Helper
private static void sortActionsIntoMenu(List<Action> actions, JMenuBar menuBar) {
actions.forEach(act -> sortActionIntoMenu(act, menuBar, new JMenu()));
}

private static Iterator<String> getMenuPath(Action act) {
Object path = act.getValue(KeyAction.PATH);
Expand Down Expand Up @@ -221,6 +209,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());
}

Expand Down Expand Up @@ -311,7 +300,7 @@ private static <T> boolean isNotForbidden(Class<T> a) {
}
// endregion

public static List<Extension> getExtensions() {
public static List<Extension<?>> getExtensions() {
if (extensions.isEmpty()) {
loadExtensions();
}
Expand Down Expand Up @@ -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<KeYGuiExtension.Tooltip> getTooltipExtensions() {
return getExtensionInstances(KeYGuiExtension.Tooltip.class);
Expand Down
Loading

0 comments on commit c482269

Please sign in to comment.