public final class ProofManagementDialog
extends javax.swing.JDialog
Modifier and Type | Class and Description |
---|---|
private static class |
ProofManagementDialog.ProofWrapper |
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.JButton |
cancelButton |
private ClassTree |
classTree |
private ContractSelectionPanel |
contractPanelByMethod |
private ContractSelectionPanel |
contractPanelByProof |
private ProofEnvironment |
env |
private InitConfig |
initConfig |
private static javax.swing.ImageIcon |
keyAlmostClosedIcon |
private static javax.swing.ImageIcon |
keyClosedIcon |
private static javax.swing.ImageIcon |
keyIcon |
private KeYMediator |
mediator |
private javax.swing.JList<ProofManagementDialog.ProofWrapper> |
proofList |
private static long |
serialVersionUID |
private javax.swing.JButton |
startButton |
private boolean |
startedProof |
private javax.swing.JTabbedPane |
tabbedPane |
private java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> |
targetIcons |
accessibleContext, rootPane, rootPaneCheckingEnabled
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
Modifier | Constructor and Description |
---|---|
private |
ProofManagementDialog(MainWindow mainWindow,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
private ProofOblInput |
createPOForSelectedContract() |
void |
dispose() |
private void |
findOrStartProof(ProofOblInput po) |
private Proof |
findPreferablyClosedProof(ProofOblInput po) |
private ContractSelectionPanel |
getActiveContractPanel() |
private Contract |
getSelectedContract() |
private boolean |
isInstanceMethodOfAbstractClass(KeYJavaType p_class,
IObserverFunction obs) |
private void |
select(KeYJavaType kjt,
IObserverFunction target) |
private void |
select(Proof p) |
private void |
selectKJTandTarget() |
static boolean |
showInstance(InitConfig initConfig)
Shows the dialog.
|
static void |
showInstance(InitConfig initConfig,
KeYJavaType selectedKJT,
IObserverFunction selectedTarget)
Shows the dialog and selects the passed
KeYJavaType and its IObserverFunction . |
private static boolean |
showInstance(InitConfig initConfig,
KeYJavaType selectedKJT,
IObserverFunction selectedTarget,
Proof selectedProof) |
static void |
showInstance(InitConfig initConfig,
Proof selectedProof)
Shows the dialog and selects the passed proof.
|
private void |
updateContractPanel() |
private void |
updateGlobalStatus() |
private void |
updateStartButton() |
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, 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 static final javax.swing.ImageIcon keyIcon
private static final javax.swing.ImageIcon keyAlmostClosedIcon
private static final javax.swing.ImageIcon keyClosedIcon
private boolean startedProof
private javax.swing.JTabbedPane tabbedPane
private java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons
private ClassTree classTree
private javax.swing.JList<ProofManagementDialog.ProofWrapper> proofList
private ContractSelectionPanel contractPanelByMethod
private ContractSelectionPanel contractPanelByProof
private javax.swing.JButton startButton
private javax.swing.JButton cancelButton
private KeYMediator mediator
private final InitConfig initConfig
private ProofEnvironment env
private ProofManagementDialog(MainWindow mainWindow, InitConfig initConfig)
public void dispose()
dispose
in class java.awt.Window
private void selectKJTandTarget()
public static void showInstance(InitConfig initConfig, Proof selectedProof)
public static void showInstance(InitConfig initConfig, KeYJavaType selectedKJT, IObserverFunction selectedTarget)
Shows the dialog and selects the passed KeYJavaType
and its IObserverFunction
.
This method is required, because the Eclipse integration of KeY needs this functionality to start a new proof for a selected method.
public static boolean showInstance(InitConfig initConfig)
private static boolean showInstance(InitConfig initConfig, KeYJavaType selectedKJT, IObserverFunction selectedTarget, Proof selectedProof)
private ContractSelectionPanel getActiveContractPanel()
private void select(KeYJavaType kjt, IObserverFunction target)
private void select(Proof p)
private Contract getSelectedContract()
private ProofOblInput createPOForSelectedContract()
private Proof findPreferablyClosedProof(ProofOblInput po)
private void findOrStartProof(ProofOblInput po)
private void updateStartButton()
private boolean isInstanceMethodOfAbstractClass(KeYJavaType p_class, IObserverFunction obs)
private void updateContractPanel()
private void updateGlobalStatus()