public class HeatmapExt extends java.lang.Object implements KeYMainMenuExtension, KeYToolbarExtension
Modifier and Type | Field and Description |
---|---|
private java.util.List<javax.swing.Action> |
actions |
private HeatmapSettingsAction |
settingsAction |
private HeatmapToggleAction |
toggleAction |
Constructor and Description |
---|
HeatmapExt() |
Modifier and Type | Method and Description |
---|---|
private java.util.List<javax.swing.Action> |
getActions(MainWindow mainWindow) |
java.util.List<javax.swing.Action> |
getMainMenuActions(MainWindow mainWindow) |
int |
getPriority() |
javax.swing.JToolBar |
getToolbar(MainWindow mainWindow) |
private java.util.List<javax.swing.Action> actions
private HeatmapToggleAction toggleAction
private HeatmapSettingsAction settingsAction
public java.util.List<javax.swing.Action> getMainMenuActions(MainWindow mainWindow)
getMainMenuActions
in interface KeYMainMenuExtension
private java.util.List<javax.swing.Action> getActions(MainWindow mainWindow)
public int getPriority()
getPriority
in interface KeYMainMenuExtension
getPriority
in interface KeYToolbarExtension
public javax.swing.JToolBar getToolbar(MainWindow mainWindow)
getToolbar
in interface KeYToolbarExtension