public class TacletOptionsSettings extends SimpleSettingsPanel implements SettingsProvider
Modifier and Type | Class and Description |
---|---|
static class |
TacletOptionsSettings.ChoiceEntry
Represents a choice with all its meta information.
|
javax.swing.JPanel.AccessibleJPanel
javax.swing.JComponent.AccessibleJComponent
lblHead, lblSubhead, pCenter, pNorth
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Constructor and Description |
---|
TacletOptionsSettings() |
Modifier and Type | Method and Description |
---|---|
protected void |
addCategory(java.lang.String cat) |
protected void |
addExplanation(java.lang.String explanation) |
void |
applySettings(MainWindow window)
The method is called if the settings should be applied to the
MainWindow . |
static java.util.List<TacletOptionsSettings.ChoiceEntry> |
createChoiceEntries(java.util.Collection<java.lang.String> choices)
Creates
TacletOptionsSettings.ChoiceEntry s for all given choices. |
static TacletOptionsSettings.ChoiceEntry |
createChoiceEntry(java.lang.String choice)
Creates a
TacletOptionsSettings.ChoiceEntry for the given choice. |
static TacletOptionsSettings.ChoiceEntry |
findChoice(java.util.List<TacletOptionsSettings.ChoiceEntry> choices,
java.lang.String choice)
Searches the choice in the given
TacletOptionsSettings.ChoiceEntry s. |
java.lang.String |
getDescription()
A textual human readable description of the settings panel.
|
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.
|
javax.swing.JComponent |
getPanel(MainWindow window)
Provides the visual component for the right side.
|
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() |
protected void |
layoutHead() |
createCheckBox, createHelpLabel, createNumberFormattedTextField, createNumberTextField, createNumberTextField, createTextArea, createTextField, demarkComponentAsErrornous, markComponentAsErrornous, setHeaderText, setSubHeaderText
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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
contains, getChildren, getIcon, getPriorityOfSettings
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.
category
- The category for which the explanation is requested.public static boolean isUnsound(java.lang.String choice)
choice
- The choice to check.true
proof will be unsound, false
proof will be
sound as long as all other choices are sound.public static boolean isIncomplete(java.lang.String choice)
choice
- The choice to check.true
proof will be incomplete, false
proof will be complete as long as all other choices are complete.public static java.lang.String getInformation(java.lang.String choice)
choice
- The choice to check.null
if no information are available.public static TacletOptionsSettings.ChoiceEntry findChoice(java.util.List<TacletOptionsSettings.ChoiceEntry> choices, java.lang.String choice)
TacletOptionsSettings.ChoiceEntry
s.choices
- The TacletOptionsSettings.ChoiceEntry
s to search in.choice
- The choice to search.TacletOptionsSettings.ChoiceEntry
for the given choice or null
otherwise.public static java.util.List<TacletOptionsSettings.ChoiceEntry> createChoiceEntries(java.util.Collection<java.lang.String> choices)
TacletOptionsSettings.ChoiceEntry
s for all given choices.choices
- The choices.TacletOptionsSettings.ChoiceEntry
s.public static TacletOptionsSettings.ChoiceEntry createChoiceEntry(java.lang.String choice)
TacletOptionsSettings.ChoiceEntry
for the given choice.choice
- The choice.TacletOptionsSettings.ChoiceEntry
.protected void layoutHead()
protected void layoutChoiceSelector()
protected void addCategory(java.lang.String cat)
protected void addExplanation(java.lang.String explanation)
public java.lang.String getDescription()
SettingsProvider
getDescription
in interface SettingsProvider
public javax.swing.JComponent getPanel(MainWindow window)
SettingsProvider
This panel will be wrapped inside a JScrollPane
.
You are allowed to reuse the return component. But then you should update the components, e.g. text field, during handling of the call.
getPanel
in interface SettingsProvider
window
- non-null referencepublic void applySettings(MainWindow window)
SettingsProvider
MainWindow
.
If the user clicks on apply or accept, the SettingsDialog
calls this method
for every registered SettingsProvider
.
You should read your values from the input components and update the settings within the main window.
If a field is not in the appropiate format, you should throw an InvalidSettingsInputException
with the reference to the panel and component.
applySettings
in interface SettingsProvider
Copyright © 2003-2019 The KeY-Project.