public final class MainWindow extends JFrame
Modifier and Type | Class and Description |
---|---|
private static class |
MainWindow.BlockingGlassPane
Glass pane that only delivers events for the status line (i.e. the abort button)
This has been partly taken from the GlassPaneDemo of the Java Tutorial
|
private class |
MainWindow.DPEnableControl |
private static class |
MainWindow.GlassPaneListener
Mouse listener for the glass pane that only delivers events for the status line (i.e. the
abort button)
This has been partly taken from the GlassPaneDemo of the Java Tutorial
|
(package private) class |
MainWindow.MainGUIListener
invoked if a frame that wants modal access is opened
|
(package private) class |
MainWindow.MainProofListener |
private class |
MainWindow.SMTInvokeAction
This action is responsible for the invocation of an SMT solver For
example the toolbar button is parameterized with an instance of this action
|
JFrame.AccessibleJFrame
Frame.AccessibleAWTFrame
Window.AccessibleAWTWindow, Window.Type
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
accessibleContext, EXIT_ON_CLOSE, rootPane, rootPaneCheckingEnabled
CROSSHAIR_CURSOR, DEFAULT_CURSOR, E_RESIZE_CURSOR, HAND_CURSOR, ICONIFIED, MAXIMIZED_BOTH, MAXIMIZED_HORIZ, MAXIMIZED_VERT, MOVE_CURSOR, N_RESIZE_CURSOR, NE_RESIZE_CURSOR, NORMAL, NW_RESIZE_CURSOR, S_RESIZE_CURSOR, SE_RESIZE_CURSOR, SW_RESIZE_CURSOR, TEXT_CURSOR, W_RESIZE_CURSOR, WAIT_CURSOR
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, HIDE_ON_CLOSE
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
Modifier | Constructor and Description |
---|---|
private |
MainWindow() |
Modifier and Type | Method and Description |
---|---|
void |
addProblem(ProofAggregate plist) |
protected void |
addRecentFile(String absolutePath) |
private void |
addToProofList(ProofAggregate plist) |
private void |
applyGnomeWorkaround()
Workaround to an issue with the Gnome window manager.
|
private JMenu |
createFileMenu() |
private JToolBar |
createFileOpsToolBar() |
private JMenu |
createHelpMenu() |
private JMenuBar |
createMenuBar()
creates menubar entries and adds them to menu bar
|
private JMenu |
createOptionsMenu() |
private JToolBar |
createProofControlToolBar() |
private JMenu |
createProofMenu() |
private ComplexButton |
createSMTComponent() |
private JMenu |
createViewMenu() |
private JComponent |
createWiderAutoModeButton() |
(package private) void |
displayResults(String message) |
private MainWindow.SMTInvokeAction |
findAction(MainWindow.SMTInvokeAction[] actions,
SolverTypeCollection union) |
void |
freezeExceptAutoModeButton()
Freeze the main window by blocking all input events, except those for the status line (i.e.
|
JToolBar |
getControlToolBar()
Returns the
JToolBar with the proof control. |
ExitMainAction |
getExitMainAction()
Returns the
ExitMainAction that is used to exit the MainWindow . |
CurrentGoalView |
getGoalView()
Returns the current goal view.
|
Action |
getHidePackagePrefixToggleAction() |
static MainWindow |
getInstance() |
static MainWindow |
getInstance(boolean ensureIsVisible) |
private KeYMediator |
getMainWindowMediator(AbstractMediatorUserInterfaceControl userInterface)
Returns the MainWindow KeyMediator.
|
KeYMediator |
getMediator()
return the mediator
|
NotificationManager |
getNotificationManager()
Returns the
NotificationManager . |
Action |
getOpenMostRecentFileAction() |
TaskTree |
getProofList() |
ProofTreeView |
getProofTreeView() |
RecentFileMenu |
getRecentFiles() |
List<Name> |
getSortedTermLabelNames() |
protected MainStatusLine |
getStatusLine() |
Action |
getUnicodeToggleAction() |
WindowUserInterfaceControl |
getUserInterface() |
TermLabelVisibilityManager |
getVisibleTermLabels() |
static boolean |
hasInstance()
Checks if an instance of the main window is already created or not.
|
private void |
layoutMain()
initialised, creates GUI and lays out the main frame
|
void |
loadPreferences(Component component)
Load the properties of the named components under
component from
the system preferences. |
void |
loadProblem(File file) |
void |
loadProblem(File file,
List<File> classPath,
File bootClassPath,
List<File> includes) |
void |
makePrettyView() |
void |
notify(NotificationEvent event)
informs the NotificationManager about an event
|
void |
openExamples() |
void |
popupInformationMessage(Object message,
String title) |
void |
popupInformationMessage(Object message,
String title,
boolean modal)
Brings up a dialog displaying a message.
|
void |
popupWarning(Object message,
String title) |
void |
savePreferences(Component component)
Store the properties of the named components under
component to
the system preferences. |
void |
selectFirstTab() |
private void |
setLaF()
Tries to set the system look and feel if this option is activated.
|
void |
setShowTacletInfo(boolean show)
Defines if talcet infos are shown or not.
|
void |
setStandardStatusLine()
Make the status line display a standard message, make progress bar and abort button invisible
|
private void |
setStandardStatusLineImmediately() |
void |
setStatusLine(String s)
Display the given message in the status line, make progress bar and abort button invisible
|
void |
setStatusLine(String str,
int max)
Display the given message in the status line, make progress bar and abort button visible, set
the progress bar range to the given value, set the current progress to zero
|
private void |
setStatusLineImmediately(String str,
int max) |
private Proof |
setUpNewProof(Proof proof) |
private JMenuItem |
setupSpeclangMenu() |
void |
syncPreferences()
Synchronised the system properties with the background storage system.
|
void |
unfreezeExceptAutoModeButton() |
private void |
updateDPSelectionMenu() |
private void |
updateDPSelectionMenu(Collection<SolverTypeCollection> unions) |
private void |
updateSequentView() |
void |
updateSMTSelectMenu()
update the selection menu for Decisionprocedures.
|
addImpl, createRootPane, frameInit, getAccessibleContext, getContentPane, getDefaultCloseOperation, getGlassPane, getGraphics, getJMenuBar, getLayeredPane, getRootPane, getTransferHandler, isDefaultLookAndFeelDecorated, isRootPaneCheckingEnabled, paramString, processWindowEvent, remove, repaint, setContentPane, setDefaultCloseOperation, setDefaultLookAndFeelDecorated, setGlassPane, setIconImage, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, setTransferHandler, update
addNotify, getCursorType, getExtendedState, getFrames, getIconImage, getMaximizedBounds, getMenuBar, getState, getTitle, isResizable, isUndecorated, remove, removeNotify, setBackground, setCursor, setExtendedState, setMaximizedBounds, setMenuBar, setOpacity, setResizable, setShape, setState, setTitle, setUndecorated
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, hide, isActive, isAlwaysOnTop, isAlwaysOnTopSupported, isAutoRequestFocus, isFocusableWindow, isFocusCycleRoot, isFocused, isLocationByPlatform, isOpaque, isShowing, isValidateRoot, pack, paint, postEvent, processEvent, processWindowFocusEvent, processWindowStateEvent, removeWindowFocusListener, removeWindowListener, removeWindowStateListener, reshape, setAlwaysOnTop, setAutoRequestFocus, setBounds, setBounds, setCursor, setFocusableWindowState, setFocusCycleRoot, setIconImages, setLocation, setLocation, setLocationByPlatform, setLocationRelativeTo, setMinimumSize, setModalExclusionType, setSize, setSize, setType, setVisible, show, toBack, 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, 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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getFont, postEvent
private static final long serialVersionUID
private static MainWindow instance
public final SequentViewSearchBar sequentViewSearchBar
public static final int TOOLBAR_ICON_SIZE
private final MainWindowTabbedPane mainWindowTabbedPane
private JToolBar controlToolBar
private JToolBar fileOpToolBar
private final MainFrame mainFrame
public final CurrentGoalView currentGoalView
private final EmptySequent emptySequent
private final JScrollPane proofListView
private final TaskTree proofList
private final KeYMediator mediator
private final WindowUserInterfaceControl userInterface
private MainStatusLine statusLine
private final MainWindow.MainProofListener proofListener
private final RecentFileMenu recentFileMenu
public boolean frozen
private static final String PARA
private final AutoModeAction autoModeAction
private OpenFileAction openFileAction
private OpenExampleAction openExampleAction
private OpenMostRecentFileAction openMostRecentFileAction
private EditMostRecentFileAction editMostRecentFileAction
private SaveFileAction saveFileAction
private QuickSaveAction quickSaveAction
private QuickLoadAction quickLoadAction
private ProofManagementAction proofManagementAction
private LemmaGenerationAction loadUserDefinedTacletsAction
private LemmaGenerationAction loadUserDefinedTacletsForProvingAction
private LemmaGenerationAction loadKeYTaclets
private LemmaGenerationBatchModeAction lemmaGenerationBatchModeAction
private final OneStepSimplificationToggleAction oneStepSimplAction
public static final String AUTO_MODE_TEXT
private final NotificationManager notificationManager
private final PreferenceSaver prefSaver
private ComplexButton smtComponent
public final JMenu smtOptions
private ExitMainAction exitMainAction
private ShowActiveSettingsAction showActiveSettingsAction
private UnicodeToggleAction unicodeToggleAction
private final HidePackagePrefixToggleAction hidePackagePrefixToggleAction
private final TermLabelMenu termLabelMenu
JCheckBoxMenuItem saveSMTFile
private boolean disableCurrentGoalView
public TermLabelVisibilityManager getVisibleTermLabels()
public static MainWindow getInstance()
public static MainWindow getInstance(boolean ensureIsVisible)
public static boolean hasInstance()
Checks if an instance of the main window is already created or not.
This method is required, because the Eclipse integration of KeY has
to do some cleanup only if a MainWindow
instance exists.
true
MainWindow
exists and is available via getInstance()
, false
MainWindow
is not instantiated and will be instantiated via getInstance()
.private void applyGnomeWorkaround()
private void setLaF()
private KeYMediator getMainWindowMediator(AbstractMediatorUserInterfaceControl userInterface)
userInterface
- The UserInterfaceControl.public KeYMediator getMediator()
private void layoutMain()
private JToolBar createFileOpsToolBar()
private JToolBar createProofControlToolBar()
private ComplexButton createSMTComponent()
private JComponent createWiderAutoModeButton()
protected MainStatusLine getStatusLine()
private void setStandardStatusLineImmediately()
public void setStandardStatusLine()
private void setStatusLineImmediately(String str, int max)
public void setStatusLine(String str, int max)
public void setStatusLine(String s)
public void selectFirstTab()
public void freezeExceptAutoModeButton()
public void unfreezeExceptAutoModeButton()
public void makePrettyView()
private void addToProofList(ProofAggregate plist)
private JMenuBar createMenuBar()
private JMenu createFileMenu()
private JMenu createViewMenu()
private JMenu createProofMenu()
private JMenu createOptionsMenu()
private JMenu createHelpMenu()
public void updateSMTSelectMenu()
private void updateDPSelectionMenu()
private MainWindow.SMTInvokeAction findAction(MainWindow.SMTInvokeAction[] actions, SolverTypeCollection union)
private void updateDPSelectionMenu(Collection<SolverTypeCollection> unions)
private JMenuItem setupSpeclangMenu()
public ProofTreeView getProofTreeView()
public CurrentGoalView getGoalView()
public void addProblem(ProofAggregate plist)
private void updateSequentView()
void displayResults(String message)
public void notify(NotificationEvent event)
event
- the NotificationEventpublic void popupInformationMessage(Object message, String title, boolean modal)
modal
- whether or not the message should be displayed in a modal dialog.public TaskTree getProofList()
public RecentFileMenu getRecentFiles()
public WindowUserInterfaceControl getUserInterface()
public Action getOpenMostRecentFileAction()
public Action getUnicodeToggleAction()
public Action getHidePackagePrefixToggleAction()
public void savePreferences(Component component)
component
to
the system preferences.
This uses the Preferences
class to access the system preferences.
Preferences are not explicitly synchronised; this happens at application
end using syncPreferences()
. All components which are in the
component tree are queried.component
- the non-null component whose preferences are to be savedPreferenceSaver
public final void loadPreferences(Component component)
component
from
the system preferences.
This uses the Preferences
class to access the system preferences.
All components which are in the component tree are queried.component
- the non-null component whose preferences are to be setPreferenceSaver
public final void syncPreferences()
PreferenceSaver
public ExitMainAction getExitMainAction()
Returns the ExitMainAction
that is used to exit the MainWindow
.
This functionality is required because for instance other projects like the Eclipse integration has to close the main window.
ExitMainAction
.public NotificationManager getNotificationManager()
Returns the NotificationManager
.
This functionality is required because in other project is it
required to execute the automatic mode without opening the result dialog
which can be disabled in the NotificationManager
.
protected void addRecentFile(String absolutePath)
public void openExamples()
public void loadProblem(File file)
public void loadProblem(File file, List<File> classPath, File bootClassPath, List<File> includes)
public JToolBar getControlToolBar()
JToolBar
with the proof control.
This method is used by the Eclipse world to add additional features!
JToolBar
with the proof control.public void setShowTacletInfo(boolean show)
Used by the Eclipse integration.
show
- true
show taclet infos, false
hide taclet infos.