de.uka.ilkd.key.gui.configuration

Class ChoiceSelector

java.lang.Object

java.awt.Component

java.awt.Container

java.awt.Window

java.awt.Dialog

javax.swing.JDialog

de.uka.ilkd.key.gui.configuration.ChoiceSelector

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible, javax.swing.RootPaneContainer, javax.swing.WindowConstants

public class ChoiceSelector
extends javax.swing.JDialog

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ChoiceSelector.ChoiceEntry Represents a choice with all its meta information.

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

javax.swing.JDialog.AccessibleJDialog

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

java.awt.Dialog.AccessibleAWTDialog, java.awt.Dialog.ModalExclusionType, java.awt.Dialog.ModalityType

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

java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type

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 java.util.HashMap<java.lang.String,java.util.Set<java.lang.String>>	category2Choices
private java.util.HashMap<java.lang.String,java.lang.String>	category2DefaultChoice
private javax.swing.JList<java.lang.String>	catList the JList with the categories of choices
private boolean	changed
private javax.swing.JList<ChoiceSelector.ChoiceEntry>	choiceList the JList with the choices for one category
private javax.swing.JTextArea	explanationArea
private static java.util.Properties	explanationMap
private static java.lang.String	EXPLANATIONS_RESOURCE
private static long	serialVersionUID
private ChoiceSettings	settings

Fields inherited from class javax.swing.JDialog

accessibleContext, rootPane, rootPaneCheckingEnabled

Fields inherited from class java.awt.Dialog

DEFAULT_MODALITY_TYPE

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface javax.swing.WindowConstants

DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, EXIT_ON_CLOSE, HIDE_ON_CLOSE

Fields inherited from interface java.awt.image.ImageObserver

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

Constructor Summary

Constructors

Constructor and Description
ChoiceSelector() creates a new ChoiceSelector
ChoiceSelector(ChoiceSettings settings) creates a new ChoiceSelector, using the ChoiceSettings from settings

Method Summary

Modifier and Type	Method and Description
static ChoiceSelector.ChoiceEntry[]	createChoiceEntries(java.util.Set<java.lang.String> choices) Creates ChoiceSelector.ChoiceEntrys for all given choices.
static ChoiceSelector.ChoiceEntry	createChoiceEntry(java.lang.String choice) Creates a ChoiceSelector.ChoiceEntry for the given choice.
static ChoiceSelector.ChoiceEntry	findChoice(ChoiceSelector.ChoiceEntry[] choices, java.lang.String choice) Searches the choice in the given ChoiceSelector.ChoiceEntrys.
static java.lang.String	getExplanation(java.lang.String category) Returns the explanation for the given category.
static java.lang.String	getInformation(java.lang.String choice) Checks if additional information for the choice are available.
static boolean	isIncomplete(java.lang.String choice) Checks if the given choice makes a proof incomplete.
static boolean	isUnsound(java.lang.String choice) Checks if the given choice makes a proof unsound.
protected void	layoutChoiceSelector() layout
private void	setChoiceList() is called if the selection of left list has changed, and causes the right one to display the possible choices for the category chosen on the left side
private void	setDefaultChoice(java.lang.String sel) is called to set the selected choice in category2DefaultChoice

Methods inherited from class javax.swing.JDialog

addImpl, createRootPane, dialogInit, getAccessibleContext, getContentPane, getDefaultCloseOperation, getGlassPane, getGraphics, getJMenuBar, getLayeredPane, getRootPane, getTransferHandler, isDefaultLookAndFeelDecorated, isRootPaneCheckingEnabled, paramString, processWindowEvent, remove, repaint, setContentPane, setDefaultCloseOperation, setDefaultLookAndFeelDecorated, setGlassPane, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, setTransferHandler, update

Methods inherited from class java.awt.Dialog

addNotify, getModalityType, getTitle, hide, isModal, isResizable, isUndecorated, setBackground, setModal, setModalityType, setOpacity, setResizable, setShape, setTitle, setUndecorated, setVisible, show, toBack

Methods inherited from class java.awt.Window

addPropertyChangeListener, addPropertyChangeListener, addWindowFocusListener, addWindowListener, addWindowStateListener, applyResourceBundle, applyResourceBundle, createBufferStrategy, createBufferStrategy, dispose, getBackground, getBufferStrategy, getFocusableWindowState, getFocusCycleRootAncestor, getFocusOwner, getFocusTraversalKeys, getIconImages, getInputContext, getListeners, getLocale, getModalExclusionType, getMostRecentFocusOwner, getOpacity, getOwnedWindows, getOwner, getOwnerlessWindows, getShape, getToolkit, getType, getWarningString, getWindowFocusListeners, getWindowListeners, getWindows, getWindowStateListeners, isActive, isAlwaysOnTop, isAlwaysOnTopSupported, isAutoRequestFocus, isFocusableWindow, isFocusCycleRoot, isFocused, isLocationByPlatform, isOpaque, isShowing, isValidateRoot, pack, paint, postEvent, processEvent, processWindowFocusEvent, processWindowStateEvent, removeNotify, removeWindowFocusListener, removeWindowListener, removeWindowStateListener, reshape, setAlwaysOnTop, setAutoRequestFocus, setBounds, setBounds, setCursor, setFocusableWindowState, setFocusCycleRoot, setIconImage, setIconImages, setLocation, setLocation, setLocationByPlatform, setLocationRelativeTo, setMinimumSize, setModalExclusionType, setSize, setSize, setType, toFront

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalPolicy, getInsets, getLayout, getMaximumSize, getMinimumSize, getMousePosition, getPreferredSize, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, print, printComponents, processContainerEvent, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusTraversalKeys, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setFont, 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, contains, createImage, createImage, createVolatileImage, createVolatileImage, disable, disableEvents, dispatchEvent, enable, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBaseline, getBaselineResizeBehavior, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, prepareImage, prepareImage, printAll, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processKeyEvent, processMouseEvent, processMouseMotionEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resize, resize, revalidate, setComponentOrientation, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setMaximumSize, setName, setPreferredSize, 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

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

EXPLANATIONS_RESOURCE

private static final java.lang.String EXPLANATIONS_RESOURCE

See Also:

Constant Field Values

settings

private ChoiceSettings settings

category2DefaultChoice

private java.util.HashMap<java.lang.String,java.lang.String> category2DefaultChoice

category2Choices

private java.util.HashMap<java.lang.String,java.util.Set<java.lang.String>> category2Choices

changed

private boolean changed

catList

private javax.swing.JList<java.lang.String> catList

the JList with the categories of choices

choiceList

private javax.swing.JList<ChoiceSelector.ChoiceEntry> choiceList

the JList with the choices for one category

explanationArea

private javax.swing.JTextArea explanationArea

explanationMap

private static java.util.Properties explanationMap

Constructor Detail

ChoiceSelector

public ChoiceSelector(ChoiceSettings settings)

creates a new ChoiceSelector, using the ChoiceSettings from settings

ChoiceSelector

public ChoiceSelector()

creates a new ChoiceSelector

Method Detail

layoutChoiceSelector

protected void layoutChoiceSelector()

layout

setDefaultChoice

private void setDefaultChoice(java.lang.String sel)

is called to set the selected choice in category2DefaultChoice

setChoiceList

private void setChoiceList()

is called if the selection of left list has changed, and causes the right one to display the possible choices for the category chosen on the left side

getExplanation

public static java.lang.String getExplanation(java.lang.String category)

Returns the explanation for the given category.

This method should be public and static because it is independent from the JDialog and it is also used by the eclipse projects.

Parameters:

category - The category for which the explanation is requested.

Returns:

The explanation for the given category.

isUnsound

public static boolean isUnsound(java.lang.String choice)

Checks if the given choice makes a proof unsound.

Parameters:

choice - The choice to check.

Returns:

true proof will be unsound, false proof will be sound as long as all other choices are sound.

isIncomplete

public static boolean isIncomplete(java.lang.String choice)

Checks if the given choice makes a proof incomplete.

Parameters:

choice - The choice to check.

Returns:

true proof will be incomplete, false proof will be complete as long as all other choices are complete.

getInformation

public static java.lang.String getInformation(java.lang.String choice)

Checks if additional information for the choice are available.

Parameters:

choice - The choice to check.

Returns:

The additional information or null if no information are available.

findChoice

public static ChoiceSelector.ChoiceEntry findChoice(ChoiceSelector.ChoiceEntry[] choices,
                                                    java.lang.String choice)

Searches the choice in the given ChoiceSelector.ChoiceEntrys.

Parameters:

choices - The ChoiceSelector.ChoiceEntrys to search in.

choice - The choice to search.

Returns:

The found ChoiceSelector.ChoiceEntry for the given choice or null otherwise.

createChoiceEntries

public static ChoiceSelector.ChoiceEntry[] createChoiceEntries(java.util.Set<java.lang.String> choices)

Creates ChoiceSelector.ChoiceEntrys for all given choices.

Parameters:

choices - The choices.

Returns:

The created ChoiceSelector.ChoiceEntrys.

createChoiceEntry

public static ChoiceSelector.ChoiceEntry createChoiceEntry(java.lang.String choice)

Creates a ChoiceSelector.ChoiceEntry for the given choice.

Parameters:

choice - The choice.

Returns:

The created ChoiceSelector.ChoiceEntry.