public final class ProofManagementDialog extends JDialog
Modifier and Type | Class and Description |
---|---|
private static class |
ProofManagementDialog.ProofWrapper |
JDialog.AccessibleJDialog
Dialog.AccessibleAWTDialog, Dialog.ModalExclusionType, Dialog.ModalityType
Window.AccessibleAWTWindow, Window.Type
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
Modifier and Type | Field and Description |
---|---|
private JButton |
cancelButton |
private ClassTree |
classTree |
private ContractSelectionPanel |
contractPanelByMethod |
private ContractSelectionPanel |
contractPanelByProof |
private ProofEnvironment |
env |
private InitConfig |
initConfig |
private static ImageIcon |
keyAlmostClosedIcon |
private static ImageIcon |
keyClosedIcon |
private static ImageIcon |
keyIcon |
private KeYMediator |
mediator |
private JList<ProofManagementDialog.ProofWrapper> |
proofList |
private static long |
serialVersionUID |
private JButton |
startButton |
private boolean |
startedProof |
private JTabbedPane |
tabbedPane |
private Map<Pair<KeYJavaType,IObserverFunction>,Icon> |
targetIcons |
accessibleContext, rootPane, rootPaneCheckingEnabled
DEFAULT_MODALITY_TYPE
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, EXIT_ON_CLOSE, HIDE_ON_CLOSE
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
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 ImageIcon keyIcon
private static final ImageIcon keyAlmostClosedIcon
private static final ImageIcon keyClosedIcon
private boolean startedProof
private JTabbedPane tabbedPane
private Map<Pair<KeYJavaType,IObserverFunction>,Icon> targetIcons
private ClassTree classTree
private JList<ProofManagementDialog.ProofWrapper> proofList
private ContractSelectionPanel contractPanelByMethod
private ContractSelectionPanel contractPanelByProof
private JButton startButton
private JButton cancelButton
private KeYMediator mediator
private final InitConfig initConfig
private ProofEnvironment env
private ProofManagementDialog(MainWindow mainWindow, InitConfig initConfig)
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()