public class GoalList extends JList<Goal>
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. |
JList.AccessibleJList, JList.DropLocation
JComponent.AccessibleJComponent
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
private static Icon |
disabledGoalIcon |
private GoalList.GoalListModel |
goalListModel |
private GoalList.GoalListGUIListener |
guiListener
listens to gui events
|
private GoalList.GoalListInteractiveListener |
interactiveListener
interactive prover listener
|
private static ImageIcon |
keyIcon |
private static 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 WeakHashMap<Sequent,String> |
seqToString |
private static long |
serialVersionUID |
HORIZONTAL_WRAP, VERTICAL, VERTICAL_WRAP
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 |
---|
GoalList(KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
private void |
goalChosen() |
private KeYMediator |
mediator() |
private JPopupMenu |
popupMenu() |
private void |
register() |
void |
removeNotify() |
private void |
selectSelectedGoal() |
private 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
private static final long serialVersionUID
private static final ImageIcon keyIcon
private static final Icon disabledGoalIcon
private static final Icon linkedGoalIcon
private KeYMediator mediator
private final GoalList.SelectingGoalListModel selectingListModel
private final GoalList.GoalListModel goalListModel
private GoalList.GoalListInteractiveListener interactiveListener
private GoalList.GoalListSelectionListener selectionListener
private GoalList.GoalListGUIListener guiListener
private static final int MAX_DISPLAYED_SEQUENT_LENGTH
private final WeakHashMap<Sequent,String> seqToString
public GoalList(KeYMediator mediator)
private JPopupMenu popupMenu()
private void setMediator(KeYMediator m)
private void register()
private void unregister()
public void removeNotify()
removeNotify
in class JComponent
private KeYMediator mediator()
private void goalChosen()
public void setVisible(boolean b)
setVisible
in class JComponent
private void selectSelectedGoal()