de.uka.ilkd.key.gui

Class ClassTree

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JTree

de.uka.ilkd.key.gui.ClassTree

All Implemented Interfaces:

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

public class ClassTree
extends javax.swing.JTree

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	ClassTree.Entry

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

javax.swing.JTree.AccessibleJTree, javax.swing.JTree.DropLocation, javax.swing.JTree.DynamicUtilTreeNode, javax.swing.JTree.EmptySelectionModel, javax.swing.JTree.TreeModelHandler, javax.swing.JTree.TreeSelectionRedirector

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 long	serialVersionUID
private Services	services
private java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon>	targetIcons

Fields inherited from class javax.swing.JTree

ANCHOR_SELECTION_PATH_PROPERTY, CELL_EDITOR_PROPERTY, CELL_RENDERER_PROPERTY, cellEditor, cellRenderer, editable, EDITABLE_PROPERTY, EXPANDS_SELECTED_PATHS_PROPERTY, INVOKES_STOP_CELL_EDITING_PROPERTY, invokesStopCellEditing, LARGE_MODEL_PROPERTY, largeModel, LEAD_SELECTION_PATH_PROPERTY, ROOT_VISIBLE_PROPERTY, rootVisible, ROW_HEIGHT_PROPERTY, rowHeight, SCROLLS_ON_EXPAND_PROPERTY, scrollsOnExpand, SELECTION_MODEL_PROPERTY, selectionModel, selectionRedirector, SHOWS_ROOT_HANDLES_PROPERTY, showsRootHandles, TOGGLE_CLICK_COUNT_PROPERTY, toggleClickCount, TREE_MODEL_PROPERTY, treeModel, treeModelListener, VISIBLE_ROW_COUNT_PROPERTY, visibleRowCount

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
ClassTree(boolean addContractTargets, boolean skipLibraryClasses, Services services)
ClassTree(boolean addContractTargets, boolean skipLibraryClasses, Services services, java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons)

Method Summary

Modifier and Type	Method and Description
private static void	compressLinearPaths(javax.swing.tree.DefaultMutableTreeNode root)
private static javax.swing.tree.DefaultMutableTreeNode	createTree(boolean addContractTargets, boolean skipLibraryClasses, Services services)
private static javax.swing.tree.DefaultMutableTreeNode	getChildByString(javax.swing.tree.DefaultMutableTreeNode parentNode, java.lang.String childString)
private static javax.swing.tree.DefaultMutableTreeNode	getChildByTarget(javax.swing.tree.DefaultMutableTreeNode parentNode, IObserverFunction target)
static java.lang.String	getDisplayName(Services services, IObserverFunction ov) Returns a human readable display name for the given ObserverFunction with use of the given Services.
javax.swing.tree.DefaultMutableTreeNode	getRootNode()
ClassTree.Entry	getSelectedEntry()
javax.swing.tree.DefaultMutableTreeNode	getSelectedNode()
private static void	insertIntoTree(javax.swing.tree.DefaultMutableTreeNode rootNode, KeYJavaType kjt, boolean addContractTargets, Services services)
private void	open(KeYJavaType kjt, IObserverFunction target)
protected javax.swing.tree.DefaultMutableTreeNode	searchNode(javax.swing.tree.DefaultMutableTreeNode parent, java.lang.String text) Searches the DefaultMutableTreeNode child with the given text.
void	select(KeYJavaType kjt)
void	select(KeYJavaType kjt, IObserverFunction target)

Methods inherited from class javax.swing.JTree

addSelectionInterval, addSelectionPath, addSelectionPaths, addSelectionRow, addSelectionRows, addTreeExpansionListener, addTreeSelectionListener, addTreeWillExpandListener, cancelEditing, clearSelection, clearToggledPaths, collapsePath, collapseRow, convertValueToText, createTreeModel, createTreeModelListener, expandPath, expandRow, fireTreeCollapsed, fireTreeExpanded, fireTreeWillCollapse, fireTreeWillExpand, fireValueChanged, getAccessibleContext, getAnchorSelectionPath, getCellEditor, getCellRenderer, getClosestPathForLocation, getClosestRowForLocation, getDefaultTreeModel, getDescendantToggledPaths, getDragEnabled, getDropLocation, getDropMode, getEditingPath, getExpandedDescendants, getExpandsSelectedPaths, getInvokesStopCellEditing, getLastSelectedPathComponent, getLeadSelectionPath, getLeadSelectionRow, getMaxSelectionRow, getMinSelectionRow, getModel, getNextMatch, getPathBetweenRows, getPathBounds, getPathForLocation, getPathForRow, getPreferredScrollableViewportSize, getRowBounds, getRowCount, getRowForLocation, getRowForPath, getRowHeight, getScrollableBlockIncrement, getScrollableTracksViewportHeight, getScrollableTracksViewportWidth, getScrollableUnitIncrement, getScrollsOnExpand, getSelectionCount, getSelectionModel, getSelectionPath, getSelectionPaths, getSelectionRows, getShowsRootHandles, getToggleClickCount, getToolTipText, getTreeExpansionListeners, getTreeSelectionListeners, getTreeWillExpandListeners, getUI, getUIClassID, getVisibleRowCount, hasBeenExpanded, isCollapsed, isCollapsed, isEditable, isEditing, isExpanded, isExpanded, isFixedRowHeight, isLargeModel, isPathEditable, isPathSelected, isRootVisible, isRowSelected, isSelectionEmpty, isVisible, makeVisible, paramString, removeDescendantSelectedPaths, removeDescendantToggledPaths, removeSelectionInterval, removeSelectionPath, removeSelectionPaths, removeSelectionRow, removeSelectionRows, removeTreeExpansionListener, removeTreeSelectionListener, removeTreeWillExpandListener, scrollPathToVisible, scrollRowToVisible, setAnchorSelectionPath, setCellEditor, setCellRenderer, setDragEnabled, setDropMode, setEditable, setExpandedState, setExpandsSelectedPaths, setInvokesStopCellEditing, setLargeModel, setLeadSelectionPath, setModel, setRootVisible, setRowHeight, setScrollsOnExpand, setSelectionInterval, setSelectionModel, setSelectionPath, setSelectionPaths, setSelectionRow, setSelectionRows, setShowsRootHandles, setToggleClickCount, setUI, setVisibleRowCount, startEditingAtPath, stopEditing, treeDidChange, updateUI

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

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

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

targetIcons

private final java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons

services

private final Services services

Constructor Detail

ClassTree

public ClassTree(boolean addContractTargets,
                 boolean skipLibraryClasses,
                 Services services,
                 java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons)

ClassTree

public ClassTree(boolean addContractTargets,
                 boolean skipLibraryClasses,
                 Services services)

Method Detail

getChildByString

private static javax.swing.tree.DefaultMutableTreeNode getChildByString(javax.swing.tree.DefaultMutableTreeNode parentNode,
                                                                        java.lang.String childString)

getChildByTarget

private static javax.swing.tree.DefaultMutableTreeNode getChildByTarget(javax.swing.tree.DefaultMutableTreeNode parentNode,
                                                                        IObserverFunction target)

insertIntoTree

private static void insertIntoTree(javax.swing.tree.DefaultMutableTreeNode rootNode,
                                   KeYJavaType kjt,
                                   boolean addContractTargets,
                                   Services services)

compressLinearPaths

private static void compressLinearPaths(javax.swing.tree.DefaultMutableTreeNode root)

getDisplayName

public static final java.lang.String getDisplayName(Services services,
                                                    IObserverFunction ov)

Returns a human readable display name for the given ObserverFunction with use of the given Services.

This functionality is also required by other products and is for that reason available as static utility method.

Parameters:

services - The Services to use.

ov - The ObserverFunction for that a display name is needed.

Returns:

The display name for the given ObserverFunction.

createTree

private static javax.swing.tree.DefaultMutableTreeNode createTree(boolean addContractTargets,
                                                                  boolean skipLibraryClasses,
                                                                  Services services)

open

private void open(KeYJavaType kjt,
                  IObserverFunction target)

searchNode

protected javax.swing.tree.DefaultMutableTreeNode searchNode(javax.swing.tree.DefaultMutableTreeNode parent,
                                                             java.lang.String text)

Searches the DefaultMutableTreeNode child with the given text.

Parameters:

parent - The DefaultMutableTreeNode to search in.

text - The text of the DefaultMutableTreeNode to search.

Returns:

The first found DefaultMutableTreeNode with the given text or null if no DefaultMutableTreeNode was found.

select

public void select(KeYJavaType kjt)

select

public void select(KeYJavaType kjt,
                   IObserverFunction target)

getRootNode

public javax.swing.tree.DefaultMutableTreeNode getRootNode()

getSelectedNode

public javax.swing.tree.DefaultMutableTreeNode getSelectedNode()

getSelectedEntry

public ClassTree.Entry getSelectedEntry()