public final class StrategySelectionView extends JPanel
This JPanel
allows to edit the StrategyProperties
of the
JavaCardDLStrategy
. The shown UI controls are generated according to
its StrategySettingsDefinition
.
There is no need to change this class to change the available
settings! The only thing to be done is to modify the available
StrategySettingsDefinition
in
JavaCardDLStrategy.Factory#getSettingsDefinition()
.
As future work this class should not show a fixed content defined by
DEFINITION
. Instead it should update the UI controls based on the
currently active proof and its Profile
since different
Profile
s support different Strategy
s with different
StrategyProperties
. For more information have a look at:
http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1359
Modifier and Type | Class and Description |
---|---|
private static class |
StrategySelectionView.StrategySelectionComponents
Provided via
StrategySelectionView#getStrategySelectionComponents() for direct
access to created user interface components. |
JPanel.AccessibleJPanel
JComponent.AccessibleJComponent
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
private StrategySelectionView.StrategySelectionComponents |
components
Allows access to shown UI controls generated according to
DEFINITION . |
private static StrategySettingsDefinition |
DEFINITION
The
StrategySettingsDefinition of FACTORY which defines
the UI controls to show. |
private static StrategyFactory |
FACTORY
The always used
StrategyFactory . |
private static String |
JAVACARDDL_STRATEGY_NAME
The name of
FACTORY . |
private KeYMediator |
mediator
The
KeYMediator which provides the active proof. |
private KeYSelectionListener |
mediatorListener
Observe changes on
mediator . |
private boolean |
predefChanged
Stores whether a chosen predef setting has been changed;
in this case, the default button should be activated again.
|
private static long |
serialVersionUID
Generated UID.
|
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
Constructor and Description |
---|
StrategySelectionView(AutoModeAction autoModeAction) |
Modifier and Type | Method and Description |
---|---|
private void |
addJavaDLOption(JPanel javaDLOptionsPanel,
Component widget,
GridBagLayout javaDLOptionsLayout,
int gridx,
int gridy,
int width) |
private void |
addJavaDLOptionSpace(JPanel javaDLOptionsPanel,
GridBagLayout javaDLOptionsLayout,
int yCoord) |
private JPanel |
createDefaultPanel(StrategySelectionView.StrategySelectionComponents components) |
protected int |
createStrategyProperty(StrategySelectionView.StrategySelectionComponents data,
StrategyFactory factory,
JPanel javaDLOptionsPanel,
GridBagLayout javaDLOptionsLayout,
int yCoord,
boolean topLevel,
AbstractStrategyPropertyDefinition definition) |
private void |
enableAll(boolean enable)
enables or disables all components
|
private void |
fixVerticalSpace(JComponent comp) |
private StrategyProperties |
getProperties() |
Strategy |
getStrategy(String strategyName,
Proof proof,
StrategyProperties properties) |
private void |
layoutPane(AutoModeAction autoModeAction)
Build everything
|
private JRadioButton |
newButton(String text,
String key,
String command,
boolean selected,
boolean enabled,
StrategyFactory factory) |
void |
refresh(Proof proof)
performs a refresh of all elements in this tab
|
private void |
refreshDefaultButton() |
void |
setMediator(KeYMediator mediator) |
private void |
updateStrategySettings(String strategyName,
StrategyProperties p) |
getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI
addAncestorListener, addNotify, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentGraphics, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getPreferredSize, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, hide, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingOrigin, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update
add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusDownCycle, validate, validateTree
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle
private static final long serialVersionUID
private static final StrategyFactory FACTORY
StrategyFactory
.private static final StrategySettingsDefinition DEFINITION
StrategySettingsDefinition
of FACTORY
which defines
the UI controls to show.private final KeYSelectionListener mediatorListener
mediator
.private KeYMediator mediator
KeYMediator
which provides the active proof.private StrategySelectionView.StrategySelectionComponents components
DEFINITION
.private boolean predefChanged
public StrategySelectionView(AutoModeAction autoModeAction)
private void layoutPane(AutoModeAction autoModeAction)
protected int createStrategyProperty(StrategySelectionView.StrategySelectionComponents data, StrategyFactory factory, JPanel javaDLOptionsPanel, GridBagLayout javaDLOptionsLayout, int yCoord, boolean topLevel, AbstractStrategyPropertyDefinition definition)
private JRadioButton newButton(String text, String key, String command, boolean selected, boolean enabled, StrategyFactory factory)
private void addJavaDLOptionSpace(JPanel javaDLOptionsPanel, GridBagLayout javaDLOptionsLayout, int yCoord)
private void addJavaDLOption(JPanel javaDLOptionsPanel, Component widget, GridBagLayout javaDLOptionsLayout, int gridx, int gridy, int width)
private void fixVerticalSpace(JComponent comp)
private JPanel createDefaultPanel(StrategySelectionView.StrategySelectionComponents components)
public void setMediator(KeYMediator mediator)
public void refresh(Proof proof)
private void refreshDefaultButton()
private void enableAll(boolean enable)
enable
- boolean saying whether to activate or deactivate the
componentspublic Strategy getStrategy(String strategyName, Proof proof, StrategyProperties properties)
private StrategyProperties getProperties()
private void updateStrategySettings(String strategyName, StrategyProperties p)