public class GoalList extends javax.swing.JList<Goal> implements KeYPaneExtension
Modifier and Type | Class and Description |
---|---|
private class |
GoalList.DisableOtherGoals
This action dis-/enables all goals except the chosen one.
|
private class |
GoalList.DisableSingleGoal
This action enables or disables a selected goal.
|
private class |
GoalList.GoalListGUIListener |
private class |
GoalList.GoalListInteractiveListener |
private static class |
GoalList.GoalListModel |
private class |
GoalList.GoalListSelectionListener |
class |
GoalList.GoalListSelectionListern
choose goal as soon as selected
|
private class |
GoalList.IconCellRenderer |
private class |
GoalList.SelectingGoalListModel
Decorate
GoalListModel with a filter that hides certain
goals. |
javax.swing.JList.AccessibleJList, javax.swing.JList.DropLocation
javax.swing.JComponent.AccessibleJComponent
Modifier and Type | Field and Description |
---|---|
private static javax.swing.Icon |
disabledGoalIcon |
static javax.swing.Icon |
GOAL_LIST_ICON |
private GoalList.GoalListModel |
goalListModel |
private GoalList.GoalListGUIListener |
guiListener
listens to gui events
|
private GoalList.GoalListInteractiveListener |
interactiveListener
interactive prover listener
|
private static javax.swing.ImageIcon |
keyIcon |
private static javax.swing.Icon |
linkedGoalIcon |
private static int |
MAX_DISPLAYED_SEQUENT_LENGTH |
private KeYMediator |
mediator |
private GoalList.SelectingGoalListModel |
selectingListModel
the model used by this view
|
private GoalList.GoalListSelectionListener |
selectionListener
KeYSelection-Listener
|
private java.util.WeakHashMap<Sequent,java.lang.String> |
seqToString |
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
Constructor and Description |
---|
GoalList() |
GoalList(KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
javax.swing.JComponent |
getComponent()
The content of the tab pane
|
javax.swing.Icon |
getIcon()
A nice icon for viewing aside to the tab title.
|
java.lang.String |
getTitle()
The title of the tab pane for the user.
|
private void |
goalChosen() |
void |
init(MainWindow window,
KeYMediator mediator) |
private KeYMediator |
mediator() |
private javax.swing.JPopupMenu |
popupMenu() |
int |
priority() |
private void |
register() |
void |
removeNotify() |
private void |
selectSelectedGoal() |
private java.lang.String |
seqToString(Sequent seq) |
private void |
setMediator(KeYMediator m)
set the KeYMediator
|
void |
setVisible(boolean b)
overrides setVisible from JFrame takes care that the view item is in the
right state
|
private void |
unregister() |
void |
updateUI() |
addListSelectionListener, addSelectionInterval, clearSelection, createSelectionModel, ensureIndexIsVisible, fireSelectionValueChanged, getAccessibleContext, getAnchorSelectionIndex, getCellBounds, getCellRenderer, getDragEnabled, getDropLocation, getDropMode, getFirstVisibleIndex, getFixedCellHeight, getFixedCellWidth, getLastVisibleIndex, getLayoutOrientation, getLeadSelectionIndex, getListSelectionListeners, getMaxSelectionIndex, getMinSelectionIndex, getModel, getNextMatch, getPreferredScrollableViewportSize, getPrototypeCellValue, getScrollableBlockIncrement, getScrollableTracksViewportHeight, getScrollableTracksViewportWidth, getScrollableUnitIncrement, getSelectedIndex, getSelectedIndices, getSelectedValue, getSelectedValues, getSelectedValuesList, getSelectionBackground, getSelectionForeground, getSelectionMode, getSelectionModel, getToolTipText, getUI, getUIClassID, getValueIsAdjusting, getVisibleRowCount, indexToLocation, isSelectedIndex, isSelectionEmpty, locationToIndex, paramString, removeListSelectionListener, removeSelectionInterval, setCellRenderer, setDragEnabled, setDropMode, setFixedCellHeight, setFixedCellWidth, setLayoutOrientation, setListData, setListData, setModel, setPrototypeCellValue, setSelectedIndex, setSelectedIndices, setSelectedValue, setSelectionBackground, setSelectionForeground, setSelectionInterval, setSelectionMode, setSelectionModel, setUI, setValueIsAdjusting, setVisibleRowCount
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, 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, 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, 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
public static final javax.swing.Icon GOAL_LIST_ICON
private static final long serialVersionUID
private static final javax.swing.ImageIcon keyIcon
private static final javax.swing.Icon disabledGoalIcon
private static final javax.swing.Icon linkedGoalIcon
private static final int MAX_DISPLAYED_SEQUENT_LENGTH
private final GoalList.SelectingGoalListModel selectingListModel
private final GoalList.GoalListModel goalListModel
private final java.util.WeakHashMap<Sequent,java.lang.String> seqToString
private KeYMediator mediator
private GoalList.GoalListInteractiveListener interactiveListener
private GoalList.GoalListSelectionListener selectionListener
private GoalList.GoalListGUIListener guiListener
public GoalList(KeYMediator mediator)
public GoalList()
public void init(MainWindow window, KeYMediator mediator)
init
in interface KeYPaneExtension
public java.lang.String getTitle()
KeYPaneExtension
getTitle
in interface KeYPaneExtension
public javax.swing.Icon getIcon()
KeYPaneExtension
getIcon
in interface KeYPaneExtension
public javax.swing.JComponent getComponent()
KeYPaneExtension
getComponent
in interface KeYPaneExtension
private javax.swing.JPopupMenu popupMenu()
private void setMediator(KeYMediator m)
public void updateUI()
updateUI
in class javax.swing.JList<Goal>
private void register()
private void unregister()
public void removeNotify()
removeNotify
in class javax.swing.JComponent
private KeYMediator mediator()
private void goalChosen()
public void setVisible(boolean b)
setVisible
in class javax.swing.JComponent
private void selectSelectedGoal()
private java.lang.String seqToString(Sequent seq)
public int priority()
priority
in interface KeYPaneExtension