de.uka.ilkd.key.gui

Class TacletMatchCompletionDialog.DataTable

java.lang.Object

java.awt.Component

java.awt.Container

javax.swing.JComponent

javax.swing.JTable

de.uka.ilkd.key.gui.TacletMatchCompletionDialog.DataTable

All Implemented Interfaces:

ModelChangeListener, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, java.util.EventListener, javax.accessibility.Accessible, javax.swing.event.CellEditorListener, javax.swing.event.ListSelectionListener, javax.swing.event.RowSorterListener, javax.swing.event.TableColumnModelListener, javax.swing.event.TableModelListener, javax.swing.Scrollable

Enclosing class:

TacletMatchCompletionDialog

private static class TacletMatchCompletionDialog.DataTable
extends javax.swing.JTable
implements ModelChangeListener

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) class	TacletMatchCompletionDialog.DataTable.InputCellRenderer
(package private) class	TacletMatchCompletionDialog.DataTable.InputEditor

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

javax.swing.JTable.AccessibleJTable, javax.swing.JTable.DropLocation, javax.swing.JTable.PrintMode

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
(package private) TacletMatchCompletionDialog.DataTable.InputEditor	iEditor
private TacletIfSelectionDialog	ifSelectionPanel the TacletIfSelectionPanel that shows the different possible instantiations of the if-sequent or a manual entered instantiation.
(package private) javax.swing.JTextArea	inputArea
(package private) TacletMatchCompletionDialog.DataTable.InputCellRenderer	iRenderer
private KeYMediator	mediator
private int	modelNr the number of the model the data table belongs to
private TacletMatchCompletionDialog	owner the enclosing dialog
private static long	serialVersionUID

Fields inherited from class javax.swing.JTable

AUTO_RESIZE_ALL_COLUMNS, AUTO_RESIZE_LAST_COLUMN, AUTO_RESIZE_NEXT_COLUMN, AUTO_RESIZE_OFF, AUTO_RESIZE_SUBSEQUENT_COLUMNS, autoCreateColumnsFromModel, autoResizeMode, cellEditor, cellSelectionEnabled, columnModel, dataModel, defaultEditorsByColumnClass, defaultRenderersByColumnClass, editingColumn, editingRow, editorComp, gridColor, preferredViewportSize, rowHeight, rowMargin, rowSelectionAllowed, selectionBackground, selectionForeground, selectionModel, showHorizontalLines, showVerticalLines, tableHeader

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

Modifier	Constructor and Description
private	DataTable(TacletMatchCompletionDialog owner, int modelNr, KeYMediator mediator)

Method Summary

Modifier and Type	Method and Description
void	editingStopped(javax.swing.event.ChangeEvent e)
javax.swing.table.TableCellEditor	getCellEditor(int row, int col) Provide sane single-click editing in table
javax.swing.table.TableCellRenderer	getCellRenderer(int row, int col)
private TacletIfSelectionDialog	getIfSelectionPanel() returns the if selection panel
int	getTotalColumnWidth()
java.lang.Object	getValueAt(int x, int y)
private boolean	hasIfSelectionPanel() returns true the model has a non empty if sequent and the ifSelectionPanel has been created and set.
void	modelChanged(ModelEvent me) this method is called if the model has changed
private void	setIfSelectionPanel(TacletIfSelectionDialog ifSelectionPanel) sets the if selection panel
private void	setUpEditor()

Methods inherited from class javax.swing.JTable

addColumn, addColumnSelectionInterval, addNotify, addRowSelectionInterval, changeSelection, clearSelection, columnAdded, columnAtPoint, columnMarginChanged, columnMoved, columnRemoved, columnSelectionChanged, configureEnclosingScrollPane, convertColumnIndexToModel, convertColumnIndexToView, convertRowIndexToModel, convertRowIndexToView, createDefaultColumnModel, createDefaultColumnsFromModel, createDefaultDataModel, createDefaultEditors, createDefaultRenderers, createDefaultSelectionModel, createDefaultTableHeader, createScrollPaneForTable, doLayout, editCellAt, editCellAt, editingCanceled, getAccessibleContext, getAutoCreateColumnsFromModel, getAutoCreateRowSorter, getAutoResizeMode, getCellEditor, getCellRect, getCellSelectionEnabled, getColumn, getColumnClass, getColumnCount, getColumnModel, getColumnName, getColumnSelectionAllowed, getDefaultEditor, getDefaultRenderer, getDragEnabled, getDropLocation, getDropMode, getEditingColumn, getEditingRow, getEditorComponent, getFillsViewportHeight, getGridColor, getIntercellSpacing, getModel, getPreferredScrollableViewportSize, getPrintable, getRowCount, getRowHeight, getRowHeight, getRowMargin, getRowSelectionAllowed, getRowSorter, getScrollableBlockIncrement, getScrollableTracksViewportHeight, getScrollableTracksViewportWidth, getScrollableUnitIncrement, getSelectedColumn, getSelectedColumnCount, getSelectedColumns, getSelectedRow, getSelectedRowCount, getSelectedRows, getSelectionBackground, getSelectionForeground, getSelectionModel, getShowHorizontalLines, getShowVerticalLines, getSurrendersFocusOnKeystroke, getTableHeader, getToolTipText, getUI, getUIClassID, getUpdateSelectionOnSort, initializeLocalVars, isCellEditable, isCellSelected, isColumnSelected, isEditing, isRowSelected, moveColumn, paramString, prepareEditor, prepareRenderer, print, print, print, print, print, processKeyBinding, removeColumn, removeColumnSelectionInterval, removeEditor, removeNotify, removeRowSelectionInterval, resizeAndRepaint, rowAtPoint, selectAll, setAutoCreateColumnsFromModel, setAutoCreateRowSorter, setAutoResizeMode, setCellEditor, setCellSelectionEnabled, setColumnModel, setColumnSelectionAllowed, setColumnSelectionInterval, setDefaultEditor, setDefaultRenderer, setDragEnabled, setDropMode, setEditingColumn, setEditingRow, setFillsViewportHeight, setGridColor, setIntercellSpacing, setModel, setPreferredScrollableViewportSize, setRowHeight, setRowHeight, setRowMargin, setRowSelectionAllowed, setRowSelectionInterval, setRowSorter, setSelectionBackground, setSelectionForeground, setSelectionMode, setSelectionModel, setShowGrid, setShowHorizontalLines, setShowVerticalLines, setSurrendersFocusOnKeystroke, setTableHeader, setUI, setUpdateSelectionOnSort, setValueAt, sizeColumnsToFit, sizeColumnsToFit, sorterChanged, tableChanged, unconfigureEnclosingScrollPane, updateUI, valueChanged

Methods inherited from class javax.swing.JComponent

addAncestorListener, 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, 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, setVisible, unregisterKeyboardAction, update

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, 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

inputArea

javax.swing.JTextArea inputArea

iEditor

final TacletMatchCompletionDialog.DataTable.InputEditor iEditor

iRenderer

final TacletMatchCompletionDialog.DataTable.InputCellRenderer iRenderer

modelNr

private int modelNr

the number of the model the data table belongs to

owner

private TacletMatchCompletionDialog owner

the enclosing dialog

mediator

private KeYMediator mediator

ifSelectionPanel

private TacletIfSelectionDialog ifSelectionPanel

the TacletIfSelectionPanel that shows the different possible instantiations of the if-sequent or a manual entered instantiation. The value is null if and only if the taclet has no if-sequent

Constructor Detail

DataTable

private DataTable(TacletMatchCompletionDialog owner,
                  int modelNr,
                  KeYMediator mediator)

Method Detail

getCellEditor

public javax.swing.table.TableCellEditor getCellEditor(int row,
                                                       int col)

Provide sane single-click editing in table

Overrides:

getCellEditor in class javax.swing.JTable

getCellRenderer

public javax.swing.table.TableCellRenderer getCellRenderer(int row,
                                                           int col)

Overrides:

getCellRenderer in class javax.swing.JTable

getValueAt

public java.lang.Object getValueAt(int x,
                                   int y)

Overrides:

getValueAt in class javax.swing.JTable

setUpEditor

private void setUpEditor()

setIfSelectionPanel

private void setIfSelectionPanel(TacletIfSelectionDialog ifSelectionPanel)

sets the if selection panel

getIfSelectionPanel

private TacletIfSelectionDialog getIfSelectionPanel()

returns the if selection panel

Returns:

the if selection panel, null if not available

hasIfSelectionPanel

private boolean hasIfSelectionPanel()

returns true the model has a non empty if sequent and the ifSelectionPanel has been created and set. So that the method getIfSelectionPanel will not return null

Returns:

true iff getIfSelectionPanel does not return null

modelChanged

public void modelChanged(ModelEvent me)

Description copied from interface: ModelChangeListener

this method is called if the model has changed

Specified by:

modelChanged in interface ModelChangeListener

getTotalColumnWidth

public int getTotalColumnWidth()

editingStopped

public void editingStopped(javax.swing.event.ChangeEvent e)

Specified by:

editingStopped in interface javax.swing.event.CellEditorListener

Overrides:

editingStopped in class javax.swing.JTable