de.uka.ilkd.key.gui

Class GoalList

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JList<Goal>

de.uka.ilkd.key.gui.GoalList

All Implemented Interfaces:

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

public class GoalList
extends javax.swing.JList<Goal>
implements KeYPaneExtension

See Also:

Serialized Form

Nested Class Summary

Nested Classes

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.

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

javax.swing.JList.AccessibleJList, javax.swing.JList.DropLocation

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 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.

Fields inherited from class javax.swing.JList

HORIZONTAL_WRAP, VERTICAL, VERTICAL_WRAP

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
GoalList()
GoalList(KeYMediator mediator)

Method Summary

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()

Methods inherited from class javax.swing.JList

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

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, 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

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

GOAL_LIST_ICON

public static final javax.swing.Icon GOAL_LIST_ICON

serialVersionUID

private static final long serialVersionUID

Generated UID.

See Also:

Constant Field Values

keyIcon

private static final javax.swing.ImageIcon keyIcon

disabledGoalIcon

private static final javax.swing.Icon disabledGoalIcon

linkedGoalIcon

private static final javax.swing.Icon linkedGoalIcon

MAX_DISPLAYED_SEQUENT_LENGTH

private static final int MAX_DISPLAYED_SEQUENT_LENGTH

See Also:

Constant Field Values

selectingListModel

private final GoalList.SelectingGoalListModel selectingListModel

the model used by this view

goalListModel

private final GoalList.GoalListModel goalListModel

seqToString

private final java.util.WeakHashMap<Sequent,java.lang.String> seqToString

mediator

private KeYMediator mediator

interactiveListener

private GoalList.GoalListInteractiveListener interactiveListener

interactive prover listener

selectionListener

private GoalList.GoalListSelectionListener selectionListener

KeYSelection-Listener

guiListener

private GoalList.GoalListGUIListener guiListener

listens to gui events

Constructor Detail

GoalList

public GoalList(KeYMediator mediator)

GoalList

public GoalList()

Method Detail

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

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:

getComponent

public javax.swing.JComponent getComponent()

Description copied from interface: KeYPaneExtension

The content of the tab pane

Specified by:

getComponent in interface KeYPaneExtension

Returns:

popupMenu

private javax.swing.JPopupMenu popupMenu()

setMediator

private void setMediator(KeYMediator m)

set the KeYMediator

updateUI

public void updateUI()

Overrides:

updateUI in class javax.swing.JList<Goal>

register

private void register()

unregister

private void unregister()

removeNotify

public void removeNotify()

Overrides:

removeNotify in class javax.swing.JComponent

mediator

private KeYMediator mediator()

goalChosen

private void goalChosen()

setVisible

public void setVisible(boolean b)

overrides setVisible from JFrame takes care that the view item is in the right state

Overrides:

setVisible in class javax.swing.JComponent

selectSelectedGoal

private void selectSelectedGoal()

seqToString

private java.lang.String seqToString(Sequent seq)

priority

public int priority()

Specified by:

priority in interface KeYPaneExtension

Returns: