public class TacletMatchCompletionDialog extends ApplyTacletDialog
Modifier and Type | Class and Description |
---|---|
(package private) class |
TacletMatchCompletionDialog.ButtonListener |
private static class |
TacletMatchCompletionDialog.DataTable |
(package private) static interface |
TacletMatchCompletionDialog.PositionSettable |
javax.swing.JDialog.AccessibleJDialog
java.awt.Dialog.AccessibleAWTDialog, java.awt.Dialog.ModalExclusionType, java.awt.Dialog.ModalityType
java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type
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 |
applyButton, cancelButton, checkAfterEachInput, mediator, model
accessibleContext, rootPane, rootPaneCheckingEnabled
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
Constructor and Description |
---|
TacletMatchCompletionDialog(MainWindow parent,
TacletInstantiationModel[] model,
Goal goal,
KeYMediator mediator) |
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
|
checkAfterEachInput, createButtonPanel, createInfoPanel, createStatusPanel, createTacletDisplay, mediator, setStatus
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
addNotify, getModalityType, getTitle, hide, isModal, isResizable, isUndecorated, setBackground, setModal, setModalityType, setOpacity, setResizable, setShape, setTitle, setUndecorated, setVisible, show, toBack
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
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
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
private static final long serialVersionUID
private TacletMatchCompletionDialog.DataTable[] dataTable
private int current
private javax.swing.JTabbedPane alternatives
private Goal goal
private javax.swing.JScrollPane tablePane
private MainWindow mainWindow
public TacletMatchCompletionDialog(MainWindow parent, TacletInstantiationModel[] model, Goal goal, KeYMediator mediator)
public void setStatus()
private void layoutDialog()
private javax.swing.JPanel createTacletPanel()
protected int current()
current
in class ApplyTacletDialog
protected void pushAllInputToModel()
pushAllInputToModel
in class ApplyTacletDialog
private void pushAllInputToModel(int i)
private javax.swing.JPanel createInstantiationDisplay(int i)
private void adaptSizes(TacletMatchCompletionDialog.DataTable dt)
private void setColumnName(int model, int col, java.lang.String name)
private void updateDataModel()
protected void closeDlg()
closeDlg
in class ApplyTacletDialog
private static java.lang.String printTerm(KeYMediator mediator, Term term)