Skip to content

Commit f3538cd

Browse files
wadoonwadoon
committed
Make the context menu more flexibel and type safe.
1 parent de96d21 commit f3538cd

14 files changed

Lines changed: 78 additions & 141 deletions

File tree

‎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 & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -3,26 +3,8 @@
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-
import de.uka.ilkd.key.rule.Rule;
106

117
/**
128
* @author Alexander Weigl
139
* @version 1 (07.04.19)
1410
*/
15-
public enum DefaultContextMenuKind implements ContextMenuKind {
16-
PROOF_LIST(Proof.class), PROOF_TREE(Node.class), TACLET_INFO(Rule.class),
17-
SEQUENT_VIEW(PosInSequent.class);
18-
19-
private final Class<?> clazz;
20-
21-
DefaultContextMenuKind(Class<?> clazz) {
22-
this.clazz = clazz;
23-
}
24-
25-
public Class<?> getType() {
26-
return clazz;
27-
}
28-
}

‎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/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) {

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
import de.uka.ilkd.key.gui.NodeInfoVisualizer;
1616
import de.uka.ilkd.key.gui.actions.KeyAction;
1717
import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
18-
import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind;
1918
import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
2019
import de.uka.ilkd.key.gui.fonticons.IconFactory;
2120
import de.uka.ilkd.key.logic.JTerm;
@@ -26,6 +25,8 @@
2625

2726
import org.key_project.prover.sequent.PosInOccurrence;
2827

28+
import org.jspecify.annotations.NonNull;
29+
2930
/**
3031
* Extension adapter for {@link OriginTermLabel}s and {@link OriginTermLabelVisualizer}s.
3132
*
@@ -59,7 +60,7 @@ private ToggleOriginHighlightAction getToggleSourceViewHighlightAction(MainWindo
5960
}
6061

6162
@Override
62-
public List<Action> getMainMenuActions(MainWindow mainWindow) {
63+
public @NonNull List<Action> getMainMenuActions(MainWindow mainWindow) {
6364
List<Action> result = new LinkedList<>();
6465
result.add(getToggleTrackingAction(mainWindow));
6566
result.add(getToggleSourceViewHighlightAction(mainWindow));
@@ -69,9 +70,9 @@ public List<Action> getMainMenuActions(MainWindow mainWindow) {
6970
@Override
7071
public List<Action> getContextActions(KeYMediator mediator, ContextMenuKind kind,
7172
Object underlyingObject) {
72-
if (kind == DefaultContextMenuKind.SEQUENT_VIEW) {
73+
if (kind == ContextMenuKind.SEQUENT_VIEW) {
7374
return Collections.singletonList(new ShowOriginAction((PosInSequent) underlyingObject));
74-
} else if (kind == DefaultContextMenuKind.PROOF_TREE
75+
} else if (kind == ContextMenuKind.PROOF_TREE
7576
&& underlyingObject instanceof Node node) {
7677
return NodeInfoVisualizer.getInstances(node).stream().map(OpenVisualizerAction::new)
7778
.collect(Collectors.toList());

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

Lines changed: 2 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
import de.uka.ilkd.key.gui.actions.KeyAction;
2020
import de.uka.ilkd.key.gui.actions.ShowProofStatistics;
2121
import de.uka.ilkd.key.gui.actions.useractions.RunStrategyOnNodeUserAction;
22-
import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind;
22+
import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
2323
import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade;
2424
import de.uka.ilkd.key.gui.fonticons.IconFactory;
2525
import de.uka.ilkd.key.gui.nodeviews.SequentViewDock;
@@ -148,7 +148,7 @@ public static JPopupMenu create(ProofTreeView view, TreePath selectedPath) {
148148
initMenu(menu, context);
149149

150150
menu.addSeparator();
151-
KeYGuiExtensionFacade.addContextMenuItems(DefaultContextMenuKind.PROOF_TREE, menu,
151+
KeYGuiExtensionFacade.addContextMenuItems(ContextMenuKind.PROOF_TREE, menu,
152152
context.invokedNode, context.mediator);
153153

154154
if (menu.getComponent(menu.getComponentCount() - 1) instanceof JPopupMenu.Separator) {
@@ -182,8 +182,6 @@ public static class ProofTreeContext {
182182
}
183183

184184
static class SubtreeStatistics extends ProofTreeAction {
185-
private static final long serialVersionUID = -8452239418108180349L;
186-
187185
protected SubtreeStatistics(ProofTreeContext context) {
188186
super(context);
189187
setName("Show Subtree Statistics");
@@ -205,8 +203,6 @@ public void actionPerformed(ActionEvent e) {
205203
}
206204

207205
static class CollapseOtherBranches extends ProofTreeAction {
208-
private static final long serialVersionUID = -6461403850298323327L;
209-
210206
protected CollapseOtherBranches(ProofTreeContext context) {
211207
super(context);
212208
setName("Collapse Other Branches");
@@ -219,8 +215,6 @@ public void actionPerformed(ActionEvent e) {
219215
}
220216

221217
static class ExpandGoalsBelow extends ProofTreeAction {
222-
private static final long serialVersionUID = -500754845710844009L;
223-
224218
protected ExpandGoalsBelow(ProofTreeContext context) {
225219
super(context);
226220
setName("Expand Goals Only Below");
@@ -252,8 +246,6 @@ public void actionPerformed(ActionEvent e) {
252246
}
253247

254248
static class ExpandAllBelow extends ProofTreeAction {
255-
private static final long serialVersionUID = 850060084128297700L;
256-
257249
public ExpandAllBelow(ProofTreeContext context) {
258250
super(context);
259251
setName("Expand All Below");
@@ -269,8 +261,6 @@ public void actionPerformed(ActionEvent e) {
269261
}
270262

271263
static class CollapseBelow extends ProofTreeAction {
272-
private static final long serialVersionUID = -7283113335781286556L;
273-
274264
public CollapseBelow(ProofTreeContext context) {
275265
super(context);
276266
setName("Collapse Below");
@@ -284,8 +274,6 @@ public void actionPerformed(ActionEvent e) {
284274
}
285275

286276
static class PrevSibling extends ProofTreeAction {
287-
private static final long serialVersionUID = 8705344500396898345L;
288-
289277
public PrevSibling(ProofTreeContext context) {
290278
super(context);
291279
setName("Previous Sibling");
@@ -321,8 +309,6 @@ public void actionPerformed(ActionEvent e) {
321309
}
322310

323311
static class NextSibling extends ProofTreeAction {
324-
private static final long serialVersionUID = 2337297147243419973L;
325-
326312
public NextSibling(ProofTreeContext context) {
327313
super(context);
328314
setName("Next Sibling");
@@ -358,8 +344,6 @@ public void actionPerformed(ActionEvent e) {
358344
}
359345

360346
static class Notes extends ProofTreeAction {
361-
private static final long serialVersionUID = -6871120844080468856L;
362-
363347
public Notes(ProofTreeContext context) {
364348
super(context);
365349
setName("Edit Notes...");
@@ -385,8 +369,6 @@ public void actionPerformed(ActionEvent e) {
385369
}
386370

387371
static class Prune extends ProofTreeAction {
388-
private static final long serialVersionUID = -1744963704210861370L;
389-
390372
public Prune(ProofTreeContext context) {
391373
super(context);
392374
setName("Prune Proof");
@@ -605,7 +587,6 @@ public void actionPerformed(ActionEvent e) {
605587
}
606588

607589
public static abstract class ProofTreeAction extends KeyAction {
608-
private static final long serialVersionUID = 2686349019163064481L;
609590
protected final ProofTreeContext context;
610591

611592
protected ProofTreeAction(ProofTreeContext context) {

0 commit comments

Comments
 (0)