de.uka.ilkd.key.gui.prooftree

Class ProofTreeSearchBar

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JPanel

de.uka.ilkd.key.gui.SearchBar

de.uka.ilkd.key.gui.prooftree.ProofTreeSearchBar

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, java.util.EventListener, javax.accessibility.Accessible, javax.swing.event.TreeModelListener

class ProofTreeSearchBar
extends SearchBar
implements javax.swing.event.TreeModelListener

Nested Class Summary

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

javax.swing.JPanel.AccessibleJPanel

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 java.util.Vector<GUIAbstractTreeNode>	cache
private int	currentRow
private ProofTreeView	proofTreeView
private static long	serialVersionUID
private int	startRow

Fields inherited from class de.uka.ilkd.key.gui.SearchBar

searchField

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
ProofTreeSearchBar(ProofTreeView proofTreeView)

Method Summary

Modifier and Type	Method and Description
void	changedUpdate(javax.swing.event.DocumentEvent e)
private boolean	containsString(java.lang.String string, java.lang.String searchString) returns true if searchString is a substring of string
private void	fillCache()
private void	fillCacheHelp(GUIBranchNode branch)
private int	getNextMatch(java.lang.String searchString, int startingRow, javax.swing.text.Position.Bias bias)
void	insertUpdate(javax.swing.event.DocumentEvent e)
void	removeUpdate(javax.swing.event.DocumentEvent e)
void	reset()
boolean	search(java.lang.String searchString)
private boolean	search(java.lang.String searchString, javax.swing.text.Position.Bias direction)
void	searchNext()
void	searchPrevious()
void	setVisible(boolean vis)
void	treeNodesChanged(javax.swing.event.TreeModelEvent e)
void	treeNodesInserted(javax.swing.event.TreeModelEvent e)
void	treeNodesRemoved(javax.swing.event.TreeModelEvent e)
void	treeStructureChanged(javax.swing.event.TreeModelEvent e)

Methods inherited from class de.uka.ilkd.key.gui.SearchBar

createUI, search

Methods inherited from class javax.swing.JPanel

getAccessibleContext, getUI, getUIClassID, paramString, setUI, 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, 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, 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

proofTreeView

private final ProofTreeView proofTreeView

startRow

private int startRow

currentRow

private int currentRow

cache

private java.util.Vector<GUIAbstractTreeNode> cache

Constructor Detail

ProofTreeSearchBar

public ProofTreeSearchBar(ProofTreeView proofTreeView)

Method Detail

setVisible

public void setVisible(boolean vis)

Overrides:

setVisible in class SearchBar

searchNext

public void searchNext()

Specified by:

searchNext in class SearchBar

searchPrevious

public void searchPrevious()

Specified by:

searchPrevious in class SearchBar

search

public boolean search(java.lang.String searchString)

Specified by:

search in class SearchBar

search

private boolean search(java.lang.String searchString,
                       javax.swing.text.Position.Bias direction)

changedUpdate

public void changedUpdate(javax.swing.event.DocumentEvent e)

insertUpdate

public void insertUpdate(javax.swing.event.DocumentEvent e)

removeUpdate

public void removeUpdate(javax.swing.event.DocumentEvent e)

treeNodesChanged

public void treeNodesChanged(javax.swing.event.TreeModelEvent e)

Specified by:

treeNodesChanged in interface javax.swing.event.TreeModelListener

treeNodesInserted

public void treeNodesInserted(javax.swing.event.TreeModelEvent e)

Specified by:

treeNodesInserted in interface javax.swing.event.TreeModelListener

treeNodesRemoved

public void treeNodesRemoved(javax.swing.event.TreeModelEvent e)

Specified by:

treeNodesRemoved in interface javax.swing.event.TreeModelListener

treeStructureChanged

public void treeStructureChanged(javax.swing.event.TreeModelEvent e)

Specified by:

treeStructureChanged in interface javax.swing.event.TreeModelListener

reset

public void reset()

fillCache

private void fillCache()

fillCacheHelp

private void fillCacheHelp(GUIBranchNode branch)

getNextMatch

private int getNextMatch(java.lang.String searchString,
                         int startingRow,
                         javax.swing.text.Position.Bias bias)

containsString

private boolean containsString(java.lang.String string,
                               java.lang.String searchString)

returns true if searchString is a substring of string

Parameters:

string - the String where to search for an occurrence of searchString

searchString - the String to be looked for

Returns:

true if a match has been found