Skip to content

Commit 18c2bff

Browse files
wadoonwadoon
authored
Make the context menu more flexibel and type safe. (#3785)
2 parents a269de1 + 5dcc7fb commit 18c2bff

16 files changed

Lines changed: 82 additions & 160 deletions

File tree

‎key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
import de.uka.ilkd.key.core.KeYSelectionEvent;
1616
import de.uka.ilkd.key.core.KeYSelectionListener;
1717
import de.uka.ilkd.key.core.KeYSelectionModel;
18-
import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind;
18+
import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
1919
import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
2020
import de.uka.ilkd.key.gui.extension.api.TabPanel;
2121
import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade;
@@ -127,7 +127,7 @@ private void checkPopup(MouseEvent e) {
127127
if (e.isPopupTrigger()) {
128128
Rule selected = infoTree.getLastSelectedPathComponent().getRule();
129129
JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu(
130-
DefaultContextMenuKind.TACLET_INFO, selected, mediator);
130+
ContextMenuKind.INFO_TREE, selected, mediator);
131131
if (menu.getComponentCount() > 0) {
132132
menu.show(InfoView.this, e.getX(), e.getY());
133133
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@
2222
import de.uka.ilkd.key.core.KeYSelectionEvent;
2323
import de.uka.ilkd.key.core.KeYSelectionListener;
2424
import de.uka.ilkd.key.gui.configuration.Config;
25-
import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind;
25+
import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
2626
import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade;
2727
import de.uka.ilkd.key.gui.fonticons.IconFactory;
2828
import de.uka.ilkd.key.gui.notification.events.AbandonTaskEvent;
@@ -303,7 +303,7 @@ private void checkPopup(MouseEvent e) {
303303
Proof p = task.proof();
304304
delegateView.setSelectionPath(selPath);
305305
JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu(
306-
DefaultContextMenuKind.PROOF_LIST, p, mediator);
306+
ContextMenuKind.PROOF_LIST, p, mediator);
307307
menu.show(e.getComponent(), e.getX(), e.getY());
308308
}
309309
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java‎

Lines changed: 5 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -8,48 +8,19 @@
88
import javax.swing.*;
99

1010
import de.uka.ilkd.key.core.KeYMediator;
11-
import de.uka.ilkd.key.pp.PosInSequent;
12-
import de.uka.ilkd.key.proof.Node;
13-
import de.uka.ilkd.key.proof.Proof;
14-
import de.uka.ilkd.key.rule.Rule;
1511

16-
import org.jspecify.annotations.NonNull;
12+
import org.jspecify.annotations.NullMarked;
13+
import org.jspecify.annotations.Nullable;
1714

1815
/**
1916
* @author Alexander Weigl
2017
* @version 1 (16.04.19)
2118
*/
19+
@NullMarked
2220
public abstract class ContextMenuAdapter implements KeYGuiExtension.ContextMenu {
23-
2421
@Override
25-
public final @NonNull List<Action> getContextActions(@NonNull KeYMediator mediator,
26-
@NonNull ContextMenuKind kind,
27-
@NonNull Object underlyingObject) {
28-
return switch ((DefaultContextMenuKind) kind) {
29-
case PROOF_LIST -> getContextActions(mediator, kind, (Proof) underlyingObject);
30-
case PROOF_TREE -> getContextActions(mediator, kind, (Node) underlyingObject);
31-
case TACLET_INFO -> getContextActions(mediator, kind, (Rule) underlyingObject);
32-
case SEQUENT_VIEW -> getContextActions(mediator, kind, (PosInSequent) underlyingObject);
33-
};
34-
}
35-
36-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
37-
Proof underlyingObject) {
38-
return Collections.emptyList();
39-
}
40-
41-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
42-
Node underlyingObject) {
43-
return Collections.emptyList();
44-
}
45-
46-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
47-
PosInSequent underlyingObject) {
48-
return Collections.emptyList();
49-
}
50-
51-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
52-
Rule underlyingObject) {
22+
public <T> List<Action> getContextActions(KeYMediator mediator, ContextMenuKind<T> kind,
23+
@Nullable T underlyingObject) {
5324
return Collections.emptyList();
5425
}
5526
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuKind.java‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,21 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.gui.extension.api;
55

6+
import de.uka.ilkd.key.pp.PosInSequent;
7+
import de.uka.ilkd.key.proof.Node;
8+
import de.uka.ilkd.key.proof.Proof;
9+
610
/**
711
* @author Alexander Weigl
812
* @version 1 (07.04.19)
913
*/
10-
public interface ContextMenuKind {
11-
Class<?> getType();
14+
public interface ContextMenuKind<T> {
15+
ContextMenuKind<Proof> PROOF_LIST = new ContextMenuKind<>() {
16+
};
17+
ContextMenuKind<Node> PROOF_TREE = new ContextMenuKind<>() {
18+
};
19+
ContextMenuKind<Object> INFO_TREE = new ContextMenuKind<>() {
20+
};
21+
ContextMenuKind<PosInSequent> SEQUENT_VIEW = new ContextMenuKind<>() {
22+
};
1223
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/DefaultContextMenuKind.java‎

Lines changed: 0 additions & 28 deletions
This file was deleted.

‎key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -164,8 +164,9 @@ interface ContextMenu {
164164
* @see de.uka.ilkd.key.gui.actions.KeyAction
165165
*/
166166
@NonNull
167-
List<Action> getContextActions(@NonNull KeYMediator mediator, @NonNull ContextMenuKind kind,
168-
@NonNull Object underlyingObject);
167+
<T> List<Action> getContextActions(@NonNull KeYMediator mediator,
168+
@NonNull ContextMenuKind<T> kind,
169+
@NonNull T underlyingObject);
169170
}
170171

171172
/**

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import de.uka.ilkd.key.settings.ViewSettings;
2020

2121
import net.miginfocom.layout.CC;
22+
import org.jspecify.annotations.NonNull;
2223

2324
/**
2425
* Extension adapter for Heatmap
@@ -36,7 +37,7 @@ public class HeatmapExt implements KeYGuiExtension, KeYGuiExtension.MainMenu,
3637
private HeatmapSettingsAction settingsAction;
3738

3839
@Override
39-
public List<Action> getMainMenuActions(MainWindow mainWindow) {
40+
public @NonNull List<Action> getMainMenuActions(MainWindow mainWindow) {
4041
return getActions(mainWindow);
4142
}
4243

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

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@
2121
import de.uka.ilkd.key.pp.PosInSequent;
2222
import de.uka.ilkd.key.proof.Proof;
2323

24+
import org.jspecify.annotations.Nullable;
25+
2426
/**
2527
* Facade for retrieving the GUI extensions.
2628
*
@@ -249,24 +251,20 @@ public static JPopupMenu createContextMenu(ContextMenuKind kind, Object underlyi
249251
return menu;
250252
}
251253

252-
public static void addContextMenuItems(ContextMenuKind kind, JPopupMenu menu,
253-
Object underlyingObject, KeYMediator mediator) {
254+
public static <T> void addContextMenuItems(ContextMenuKind<T> kind, JPopupMenu menu,
255+
T underlyingObject, KeYMediator mediator) {
254256
getContextMenuItems(kind, underlyingObject, mediator)
255257
.forEach(it -> sortActionIntoMenu(it, menu));
256258
}
257259

258-
public static List<Action> getContextMenuItems(ContextMenuKind kind, Object underlyingObject,
259-
KeYMediator mediator) {
260-
if (!kind.getType().isAssignableFrom(underlyingObject.getClass())) {
261-
throw new IllegalArgumentException();
262-
}
263-
260+
public static <T> List<Action> getContextMenuItems(ContextMenuKind<T> kind,
261+
@Nullable T underlyingObject, KeYMediator mediator) {
264262
return getContextMenuExtensions().stream()
265263
.flatMap(it -> it.getContextActions(mediator, kind, underlyingObject).stream())
266264
.collect(Collectors.toList());
267265
}
268266

269-
public static JMenu createTermMenu(ContextMenuKind kind, Object underlyingObject,
267+
public static <T> JMenu createTermMenu(ContextMenuKind<T> kind, T underlyingObject,
270268
KeYMediator mediator) {
271269
JMenu menu = new JMenu("Extensions");
272270
getContextMenuItems(kind, underlyingObject, mediator)

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

Lines changed: 10 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -20,14 +20,10 @@
2020
import de.uka.ilkd.key.gui.extension.api.TabPanel;
2121
import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid;
2222
import de.uka.ilkd.key.gui.fonticons.IconFontSwing;
23-
import de.uka.ilkd.key.gui.settings.InvalidSettingsInputException;
2423
import de.uka.ilkd.key.gui.settings.SettingsProvider;
25-
import de.uka.ilkd.key.pp.PosInSequent;
26-
import de.uka.ilkd.key.proof.Node;
27-
import de.uka.ilkd.key.proof.Proof;
28-
import de.uka.ilkd.key.rule.Rule;
2924

30-
import org.jspecify.annotations.NonNull;
25+
import org.jspecify.annotations.NullMarked;
26+
import org.jspecify.annotations.Nullable;
3127
import org.slf4j.Logger;
3228
import org.slf4j.LoggerFactory;
3329

@@ -38,6 +34,7 @@
3834
@KeYGuiExtension.Info(name = "Test Extension",
3935
description = "Should only be used for testing of the extension facade", priority = 100000,
4036
optional = true)
37+
@NullMarked
4138
public class TestExtension implements KeYGuiExtension, KeYGuiExtension.MainMenu,
4239
KeYGuiExtension.LeftPanel, KeYGuiExtension.StatusLine, KeYGuiExtension.ContextMenu,
4340
KeYGuiExtension.Toolbar, KeYGuiExtension.KeyboardShortcuts, KeYGuiExtension.Settings {
@@ -47,26 +44,8 @@ public class TestExtension implements KeYGuiExtension, KeYGuiExtension.MainMenu,
4744
private final KeyAction actionTest = new TestAction();
4845
private final ContextMenuAdapter cmAdapter = new ContextMenuAdapter() {
4946
@Override
50-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
51-
Proof underlyingObject) {
52-
return Collections.singletonList(actionTest);
53-
}
54-
55-
@Override
56-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
57-
Node underlyingObject) {
58-
return Collections.singletonList(actionTest);
59-
}
60-
61-
@Override
62-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
63-
PosInSequent underlyingObject) {
64-
return Collections.singletonList(actionTest);
65-
}
66-
67-
@Override
68-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
69-
Rule underlyingObject) {
47+
public <T> List<Action> getContextActions(KeYMediator mediator, ContextMenuKind<T> kind,
48+
@Nullable T underlyingObject) {
7049
return Collections.singletonList(actionTest);
7150
}
7251
};
@@ -77,8 +56,8 @@ public List<Action> getMainMenuActions(MainWindow mainWindow) {
7756
}
7857

7958
@Override
80-
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
81-
Object underlyingObject) {
59+
public <T> List<Action> getContextActions(KeYMediator mediator, ContextMenuKind<T> kind,
60+
@Nullable T underlyingObject) {
8261
return cmAdapter.getContextActions(mediator, kind, underlyingObject);
8362
}
8463

@@ -100,8 +79,8 @@ public SettingsProvider getSettings() {
10079
}
10180

10281
@Override
103-
public @NonNull Collection<TabPanel> getPanels(@NonNull MainWindow window,
104-
@NonNull KeYMediator mediator) {
82+
public Collection<TabPanel> getPanels(MainWindow window,
83+
KeYMediator mediator) {
10584
return Collections.singleton(new TabPanel() {
10685
@Override
10786
public String getTitle() {
@@ -122,8 +101,6 @@ public Collection<Action> getShortcuts(KeYMediator mediator, String componentId,
122101
}
123102

124103
private static class TestAction extends KeyAction {
125-
private static final long serialVersionUID = -2701623640497343330L;
126-
127104
public TestAction() {
128105
setName("Test");
129106
setMenuPath("Test.Test.Test");
@@ -153,7 +130,7 @@ public JPanel getPanel(MainWindow window) {
153130
}
154131

155132
@Override
156-
public void applySettings(MainWindow window) throws InvalidSettingsInputException {
133+
public void applySettings(MainWindow window) {
157134
LOGGER.trace("TestSettingsProvider.applySettings");
158135
}
159136
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewMenu.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
import javax.swing.*;
99

1010
import de.uka.ilkd.key.gui.actions.KeyAction;
11-
import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind;
11+
import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
1212
import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade;
1313
import de.uka.ilkd.key.gui.utilities.GuiUtilities;
1414
import de.uka.ilkd.key.logic.NameCreationInfo;
@@ -81,7 +81,7 @@ protected T getSequentView() {
8181
*/
8282
protected void addExtensionMenu() {
8383
List<Action> actions =
84-
KeYGuiExtensionFacade.getContextMenuItems(DefaultContextMenuKind.SEQUENT_VIEW, getPos(),
84+
KeYGuiExtensionFacade.getContextMenuItems(ContextMenuKind.SEQUENT_VIEW, getPos(),
8585
getSequentView().getMainWindow().getMediator());
8686

8787
for (Action action : actions) {

0 commit comments

Comments
 (0)