class ProofTreeSearchBar extends SearchBar implements javax.swing.event.TreeModelListener
javax.swing.JPanel.AccessibleJPanel
javax.swing.JComponent.AccessibleJComponent
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 |
searchField
listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW
Constructor and Description |
---|
ProofTreeSearchBar(ProofTreeView proofTreeView) |
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) |
getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI
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
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 final ProofTreeView proofTreeView
private int startRow
private int currentRow
private java.util.Vector<GUIAbstractTreeNode> cache
public ProofTreeSearchBar(ProofTreeView proofTreeView)
public void setVisible(boolean vis)
setVisible
in class SearchBar
public void searchNext()
searchNext
in class SearchBar
public void searchPrevious()
searchPrevious
in class SearchBar
private boolean search(java.lang.String searchString, javax.swing.text.Position.Bias direction)
public void changedUpdate(javax.swing.event.DocumentEvent e)
public void insertUpdate(javax.swing.event.DocumentEvent e)
public void removeUpdate(javax.swing.event.DocumentEvent e)
public void treeNodesChanged(javax.swing.event.TreeModelEvent e)
treeNodesChanged
in interface javax.swing.event.TreeModelListener
public void treeNodesInserted(javax.swing.event.TreeModelEvent e)
treeNodesInserted
in interface javax.swing.event.TreeModelListener
public void treeNodesRemoved(javax.swing.event.TreeModelEvent e)
treeNodesRemoved
in interface javax.swing.event.TreeModelListener
public void treeStructureChanged(javax.swing.event.TreeModelEvent e)
treeStructureChanged
in interface javax.swing.event.TreeModelListener
public void reset()
private void fillCache()
private void fillCacheHelp(GUIBranchNode branch)
private int getNextMatch(java.lang.String searchString, int startingRow, javax.swing.text.Position.Bias bias)
private boolean containsString(java.lang.String string, java.lang.String searchString)
string
- the String where to search for an occurrence of searchStringsearchString
- the String to be looked for