de.uka.ilkd.key.gui

Class TacletMatchCompletionDialog

java.lang.Object

java.awt.Component

java.awt.Container

java.awt.Window

java.awt.Dialog

javax.swing.JDialog

de.uka.ilkd.key.gui.ApplyTacletDialog

de.uka.ilkd.key.gui.TacletMatchCompletionDialog

All Implemented Interfaces:

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

public class TacletMatchCompletionDialog
extends ApplyTacletDialog

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) class	TacletMatchCompletionDialog.ButtonListener
private static class	TacletMatchCompletionDialog.DataTable
(package private) static interface	TacletMatchCompletionDialog.PositionSettable

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

javax.swing.JDialog.AccessibleJDialog

Nested classes/interfaces inherited from class java.awt.Dialog

java.awt.Dialog.AccessibleAWTDialog, java.awt.Dialog.ModalExclusionType, java.awt.Dialog.ModalityType

Nested classes/interfaces inherited from class java.awt.Window

java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type

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 javax.swing.JTabbedPane	alternatives
private int	current
private TacletMatchCompletionDialog.DataTable[]	dataTable
private Goal	goal the goal the application of the rule has to be performed
private MainWindow	mainWindow
private static long	serialVersionUID
private javax.swing.JScrollPane	tablePane

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

applyButton, cancelButton, checkAfterEachInput, mediator, model

Fields inherited from class javax.swing.JDialog

accessibleContext, rootPane, rootPaneCheckingEnabled

Fields inherited from class java.awt.Dialog

DEFAULT_MODALITY_TYPE

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface javax.swing.WindowConstants

DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, EXIT_ON_CLOSE, HIDE_ON_CLOSE

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

Constructors

Constructor and Description
TacletMatchCompletionDialog(MainWindow parent, TacletInstantiationModel[] model, Goal goal, KeYMediator mediator)

Method Summary

Modifier and Type	Method and Description
private void	adaptSizes(TacletMatchCompletionDialog.DataTable dt)
protected void	closeDlg() save the preferences of this window prior to closing it.
private javax.swing.JPanel	createInstantiationDisplay(int i)
private javax.swing.JPanel	createTacletPanel()
protected int	current() returns the current selected model
private void	layoutDialog()
private static java.lang.String	printTerm(KeYMediator mediator, Term term)
protected void	pushAllInputToModel()
private void	pushAllInputToModel(int i)
private void	setColumnName(int model, int col, java.lang.String name)
void	setStatus() update the status by the current model element.
private void	updateDataModel() shows next instantiation suggestion

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

checkAfterEachInput, createButtonPanel, createInfoPanel, createStatusPanel, createTacletDisplay, mediator, setStatus

Methods inherited from class javax.swing.JDialog

addImpl, createRootPane, dialogInit, getAccessibleContext, getContentPane, getDefaultCloseOperation, getGlassPane, getGraphics, getJMenuBar, getLayeredPane, getRootPane, getTransferHandler, isDefaultLookAndFeelDecorated, isRootPaneCheckingEnabled, paramString, processWindowEvent, remove, repaint, setContentPane, setDefaultCloseOperation, setDefaultLookAndFeelDecorated, setGlassPane, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, setTransferHandler, update

Methods inherited from class java.awt.Dialog

addNotify, getModalityType, getTitle, hide, isModal, isResizable, isUndecorated, setBackground, setModal, setModalityType, setOpacity, setResizable, setShape, setTitle, setUndecorated, setVisible, show, toBack

Methods inherited from class java.awt.Window

addPropertyChangeListener, addPropertyChangeListener, addWindowFocusListener, addWindowListener, addWindowStateListener, applyResourceBundle, applyResourceBundle, createBufferStrategy, createBufferStrategy, dispose, getBackground, getBufferStrategy, getFocusableWindowState, getFocusCycleRootAncestor, getFocusOwner, getFocusTraversalKeys, getIconImages, getInputContext, getListeners, getLocale, getModalExclusionType, getMostRecentFocusOwner, getOpacity, getOwnedWindows, getOwner, getOwnerlessWindows, getShape, getToolkit, getType, getWarningString, getWindowFocusListeners, getWindowListeners, getWindows, getWindowStateListeners, isActive, isAlwaysOnTop, isAlwaysOnTopSupported, isAutoRequestFocus, isFocusableWindow, isFocusCycleRoot, isFocused, isLocationByPlatform, isOpaque, isShowing, isValidateRoot, pack, paint, postEvent, processEvent, processWindowFocusEvent, processWindowStateEvent, removeNotify, removeWindowFocusListener, removeWindowListener, removeWindowStateListener, reshape, setAlwaysOnTop, setAutoRequestFocus, setBounds, setBounds, setCursor, setFocusableWindowState, setFocusCycleRoot, setIconImage, setIconImages, setLocation, setLocation, setLocationByPlatform, setLocationRelativeTo, setMinimumSize, setModalExclusionType, setSize, setSize, setType, toFront

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalPolicy, getInsets, getLayout, getMaximumSize, getMinimumSize, getMousePosition, getPreferredSize, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, print, printComponents, processContainerEvent, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusTraversalKeys, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setFont, 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, contains, createImage, createImage, createVolatileImage, createVolatileImage, disable, disableEvents, dispatchEvent, enable, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBaseline, getBaselineResizeBehavior, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, prepareImage, prepareImage, printAll, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processKeyEvent, processMouseEvent, processMouseMotionEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resize, resize, revalidate, setComponentOrientation, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setMaximumSize, setName, setPreferredSize, 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

dataTable

private TacletMatchCompletionDialog.DataTable[] dataTable

current

private int current

alternatives

private javax.swing.JTabbedPane alternatives

goal

private Goal goal

the goal the application of the rule has to be performed

tablePane

private javax.swing.JScrollPane tablePane

mainWindow

private MainWindow mainWindow

Constructor Detail

TacletMatchCompletionDialog

public TacletMatchCompletionDialog(MainWindow parent,
                                   TacletInstantiationModel[] model,
                                   Goal goal,
                                   KeYMediator mediator)

Method Detail

setStatus

public void setStatus()

update the status by the current model element.

layoutDialog

private void layoutDialog()

createTacletPanel

private javax.swing.JPanel createTacletPanel()

current

protected int current()

returns the current selected model

Specified by:

current in class ApplyTacletDialog

Returns:

the current selected model

pushAllInputToModel

protected void pushAllInputToModel()

Specified by:

pushAllInputToModel in class ApplyTacletDialog

pushAllInputToModel

private void pushAllInputToModel(int i)

createInstantiationDisplay

private javax.swing.JPanel createInstantiationDisplay(int i)

adaptSizes

private void adaptSizes(TacletMatchCompletionDialog.DataTable dt)

setColumnName

private void setColumnName(int model,
                           int col,
                           java.lang.String name)

updateDataModel

private void updateDataModel()

shows next instantiation suggestion

closeDlg

protected void closeDlg()

save the preferences of this window prior to closing it.

Overrides:

closeDlg in class ApplyTacletDialog

printTerm

private static java.lang.String printTerm(KeYMediator mediator,
                                          Term term)