de.uka.ilkd.key.gui

Class StrategySelectionView

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JPanel

de.uka.ilkd.key.gui.StrategySelectionView

All Implemented Interfaces:

KeYPaneExtension, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible

public final class StrategySelectionView
extends javax.swing.JPanel
implements KeYPaneExtension

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 Profiles support different Strategys with different StrategyProperties. For more information have a look at: http://i12www.iti.kit.edu/~klebanov/mantis/view.php?id=1359

Author:

Martin Hentschel

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	StrategySelectionView.StrategySelectionComponents Provided via StrategySelectionView#getStrategySelectionComponents() for direct access to created user interface components.

Nested classes/interfaces inherited from class javax.swing.JPanel

javax.swing.JPanel.AccessibleJPanel

Nested classes/interfaces inherited from class javax.swing.JComponent

javax.swing.JComponent.AccessibleJComponent

Nested classes/interfaces inherited from class java.awt.Container

java.awt.Container.AccessibleAWTContainer

Nested classes/interfaces inherited from class java.awt.Component

java.awt.Component.AccessibleAWTComponent, java.awt.Component.BaselineResizeBehavior, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy

Field Summary

Fields

Modifier and Type	Field and Description
private javax.swing.JButton	btnGo
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 java.lang.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.
static javax.swing.Icon	PROOF_SEARCH_STRATEGY_ICON
private static long	serialVersionUID Generated UID.

Fields inherited from class javax.swing.JComponent

listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

Fields inherited from class java.awt.Component

accessibleContext, BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

Constructors

Constructor and Description
StrategySelectionView()

Method Summary

Modifier and Type	Method and Description
private void	addJavaDLOption(javax.swing.JPanel javaDLOptionsPanel, java.awt.Component widget, java.awt.GridBagLayout javaDLOptionsLayout, int gridx, int gridy, int width)
private void	addJavaDLOptionSpace(javax.swing.JPanel javaDLOptionsPanel, java.awt.GridBagLayout javaDLOptionsLayout, int yCoord)
private javax.swing.JPanel	createDefaultPanel(StrategySelectionView.StrategySelectionComponents components)
protected int	createStrategyProperty(StrategySelectionView.StrategySelectionComponents data, StrategyFactory factory, javax.swing.JPanel javaDLOptionsPanel, java.awt.GridBagLayout javaDLOptionsLayout, int yCoord, boolean topLevel, AbstractStrategyPropertyDefinition definition)
private void	enableAll(boolean enable) enables or disables all components
private void	fixVerticalSpace(javax.swing.JComponent comp)
javax.swing.JComponent	getComponent() The content of the tab pane
javax.swing.Icon	getIcon() A nice icon for viewing aside to the tab title.
private StrategyProperties	getProperties()
Strategy	getStrategy(java.lang.String strategyName, Proof proof, StrategyProperties properties)
java.lang.String	getTitle() The title of the tab pane for the user.
void	init(MainWindow window, KeYMediator mediator)
private void	layoutPane() Build everything
private javax.swing.JRadioButton	newButton(java.lang.String text, java.lang.String key, java.lang.String command, boolean selected, boolean enabled, StrategyFactory factory)
int	priority()
void	refresh(Proof proof) performs a refresh of all elements in this tab
private void	refreshDefaultButton()
void	setMediator(KeYMediator mediator)
private void	updateStrategySettings(java.lang.String strategyName, StrategyProperties p)

Methods inherited from class javax.swing.JPanel

getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI

Methods inherited from class javax.swing.JComponent

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

Methods inherited from class java.awt.Container

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

Methods inherited from class java.awt.Component

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

PROOF_SEARCH_STRATEGY_ICON

public static final javax.swing.Icon PROOF_SEARCH_STRATEGY_ICON

serialVersionUID

private static final long serialVersionUID

Generated UID.

See Also:

Constant Field Values

FACTORY

private static final StrategyFactory FACTORY

The always used StrategyFactory.

DEFINITION

private static final StrategySettingsDefinition DEFINITION

The StrategySettingsDefinition of FACTORY which defines the UI controls to show.

JAVACARDDL_STRATEGY_NAME

private static final java.lang.String JAVACARDDL_STRATEGY_NAME

The name of FACTORY.

mediator

private KeYMediator mediator

The KeYMediator which provides the active proof.

components

private StrategySelectionView.StrategySelectionComponents components

Allows access to shown UI controls generated according to DEFINITION.

predefChanged

private boolean predefChanged

Stores whether a chosen predef setting has been changed; in this case, the default button should be activated again.

mediatorListener

private final KeYSelectionListener mediatorListener

Observe changes on mediator.

btnGo

private javax.swing.JButton btnGo

Constructor Detail

StrategySelectionView

public StrategySelectionView()

Method Detail

layoutPane

private void layoutPane()

Build everything

createStrategyProperty

protected int createStrategyProperty(StrategySelectionView.StrategySelectionComponents data,
                                     StrategyFactory factory,
                                     javax.swing.JPanel javaDLOptionsPanel,
                                     java.awt.GridBagLayout javaDLOptionsLayout,
                                     int yCoord,
                                     boolean topLevel,
                                     AbstractStrategyPropertyDefinition definition)

newButton

private javax.swing.JRadioButton newButton(java.lang.String text,
                                           java.lang.String key,
                                           java.lang.String command,
                                           boolean selected,
                                           boolean enabled,
                                           StrategyFactory factory)

addJavaDLOptionSpace

private void addJavaDLOptionSpace(javax.swing.JPanel javaDLOptionsPanel,
                                  java.awt.GridBagLayout javaDLOptionsLayout,
                                  int yCoord)

addJavaDLOption

private void addJavaDLOption(javax.swing.JPanel javaDLOptionsPanel,
                             java.awt.Component widget,
                             java.awt.GridBagLayout javaDLOptionsLayout,
                             int gridx,
                             int gridy,
                             int width)

fixVerticalSpace

private void fixVerticalSpace(javax.swing.JComponent comp)

createDefaultPanel

private javax.swing.JPanel createDefaultPanel(StrategySelectionView.StrategySelectionComponents components)

setMediator

public void setMediator(KeYMediator mediator)

refresh

public void refresh(Proof proof)

performs a refresh of all elements in this tab

refreshDefaultButton

private void refreshDefaultButton()

enableAll

private void enableAll(boolean enable)

enables or disables all components

Parameters:

enable - boolean saying whether to activate or deactivate the components

getStrategy

public Strategy getStrategy(java.lang.String strategyName,
                            Proof proof,
                            StrategyProperties properties)

getProperties

private StrategyProperties getProperties()

Returns:

the StrategyProperties

updateStrategySettings

private void updateStrategySettings(java.lang.String strategyName,
                                    StrategyProperties p)

init

public void init(MainWindow window,
                 KeYMediator mediator)

Specified by:

init in interface KeYPaneExtension

getTitle

public java.lang.String getTitle()

Description copied from interface: KeYPaneExtension

The title of the tab pane for the user.

Specified by:

getTitle in interface KeYPaneExtension

Returns:

non-null and non-empty string

getComponent

public javax.swing.JComponent getComponent()

Description copied from interface: KeYPaneExtension

The content of the tab pane

Specified by:

getComponent in interface KeYPaneExtension

Returns:

priority

public int priority()

Specified by:

priority in interface KeYPaneExtension

Returns:

getIcon

public javax.swing.Icon getIcon()

Description copied from interface: KeYPaneExtension

A nice icon for viewing aside to the tab title.

Specified by:

getIcon in interface KeYPaneExtension

Returns: