public final class MainWindow
extends javax.swing.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
|
javax.swing.JFrame.AccessibleJFrame
java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
AUTO_MODE_TEXT |
private AutoModeAction |
autoModeAction
action for starting and stopping automatic mode
|
private javax.swing.JToolBar |
controlToolBar
the first toolbar
|
CurrentGoalView |
currentGoalView
SequentView for the current goal
|
private boolean |
disableCurrentGoalView
set to true if the view of the current goal should not be updated
|
private EditMostRecentFileAction |
editMostRecentFileAction
action for editing the most recent KeY file
|
private EmptySequent |
emptySequent
Use this SequentView in case no proof is loaded.
|
private ExitMainAction |
exitMainAction |
private javax.swing.JToolBar |
fileOpToolBar
the second toolbar
|
boolean |
frozen |
private HidePackagePrefixToggleAction |
hidePackagePrefixToggleAction |
private static MainWindow |
instance |
private LemmaGenerationBatchModeAction |
lemmaGenerationBatchModeAction |
private LemmaGenerationAction |
loadKeYTaclets |
private LemmaGenerationAction |
loadUserDefinedTacletsAction
action for loading taclets onto a ongoing proof
|
private LemmaGenerationAction |
loadUserDefinedTacletsForProvingAction |
private MainFrame |
mainFrame
JScrollPane for displaying SequentViews
|
private MainWindowTabbedPane |
mainWindowTabbedPane
the tab bar at the left
|
private KeYMediator |
mediator
the mediator is stored here
|
private NotificationManager |
notificationManager |
private OpenExampleAction |
openExampleAction
action for opening an example
|
private OpenFileAction |
openFileAction
action for opening a KeY file
|
private OpenMostRecentFileAction |
openMostRecentFileAction
action for opening the most recent KeY file
|
private static java.lang.String |
PARA |
private PreferenceSaver |
prefSaver |
private TaskTree |
proofList |
private MainWindow.MainProofListener |
proofListener
listener to global proof events
|
private javax.swing.JScrollPane |
proofListView
contains a list of all proofs
|
private ProofManagementAction |
proofManagementAction
action for opening the proof management dialog
|
private QuickLoadAction |
quickLoadAction |
private QuickSaveAction |
quickSaveAction |
private RecentFileMenu |
recentFileMenu |
private SaveFileAction |
saveFileAction
action for saving a proof (attempt)
|
(package private) javax.swing.JCheckBoxMenuItem |
saveSMTFile |
SequentViewSearchBar |
sequentViewSearchBar
Search bar for Sequent Views.
|
private static long |
serialVersionUID |
private ShowActiveSettingsAction |
showActiveSettingsAction |
private ComplexButton |
smtComponent |
javax.swing.JMenu |
smtOptions
The menu for the SMT solver options
|
private javax.swing.JComponent |
sourceView
the view to show source code and symbolic execution information
|
private MainStatusLine |
statusLine
the status line
|
private TermLabelMenu |
termLabelMenu |
static int |
TOOLBAR_ICON_SIZE
size of the tool bar icons
|
private UnicodeToggleAction |
unicodeToggleAction |
private WindowUserInterfaceControl |
userInterface
the user interface which direct all notifications to this window
|
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
Modifier | Constructor and Description |
---|---|
private |
MainWindow() |
Modifier and Type | Method and Description |
---|---|
void |
addProblem(ProofAggregate plist) |
protected void |
addRecentFile(java.lang.String absolutePath) |
private void |
addToProofList(ProofAggregate plist) |
private void |
applyGnomeWorkaround()
Workaround to an issue with the Gnome window manager.
|
private void |
createExtensionMenu(javax.swing.JMenuBar menuBar) |
private javax.swing.JMenu |
createFileMenu() |
private javax.swing.JToolBar |
createFileOpsToolBar() |
private javax.swing.JMenu |
createHelpMenu() |
private javax.swing.JMenuBar |
createMenuBar()
creates menubar entries and adds them to menu bar
|
private javax.swing.JMenu |
createOptionsMenu() |
private javax.swing.JToolBar |
createProofControlToolBar() |
private javax.swing.JMenu |
createProofMenu() |
private ComplexButton |
createSMTComponent() |
private javax.swing.JMenu |
createViewMenu() |
private javax.swing.JComponent |
createWiderAutoModeButton() |
(package private) void |
displayResults(java.lang.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.
|
AutoModeAction |
getAutoModeAction() |
javax.swing.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.
|
javax.swing.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 . |
javax.swing.Action |
getOpenMostRecentFileAction() |
TaskTree |
getProofList() |
ProofTreeView |
getProofTreeView() |
RecentFileMenu |
getRecentFiles() |
java.util.List<Name> |
getSortedTermLabelNames() |
protected MainStatusLine |
getStatusLine() |
javax.swing.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(java.awt.Component component)
Load the properties of the named components under
component from
the system preferences. |
void |
loadProblem(java.io.File file) |
void |
loadProblem(java.io.File file,
java.util.List<java.io.File> classPath,
java.io.File bootClassPath,
java.util.List<java.io.File> includes) |
void |
makePrettyView() |
void |
notify(NotificationEvent event)
informs the NotificationManager about an event
|
void |
openExamples() |
void |
popupInformationMessage(java.lang.Object message,
java.lang.String title) |
void |
popupInformationMessage(java.lang.Object message,
java.lang.String title,
boolean modal)
Brings up a dialog displaying a message.
|
void |
popupWarning(java.lang.Object message,
java.lang.String title) |
void |
savePreferences(java.awt.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(java.lang.String s)
Display the given message in the status line, make progress bar and abort button invisible
|
void |
setStatusLine(java.lang.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(java.lang.String str,
int max) |
private Proof |
setUpNewProof(Proof proof) |
private javax.swing.JMenuItem |
setupSpeclangMenu() |
void |
syncPreferences()
Synchronised the system properties with the background storage system.
|
void |
unfreezeExceptAutoModeButton() |
private void |
updateDPSelectionMenu() |
private void |
updateDPSelectionMenu(java.util.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
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 javax.swing.JToolBar controlToolBar
private javax.swing.JToolBar fileOpToolBar
private final MainFrame mainFrame
private final javax.swing.JComponent sourceView
public final CurrentGoalView currentGoalView
private final EmptySequent emptySequent
private final javax.swing.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 java.lang.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
public static final java.lang.String AUTO_MODE_TEXT
private final NotificationManager notificationManager
private final PreferenceSaver prefSaver
private ComplexButton smtComponent
public final javax.swing.JMenu smtOptions
private ExitMainAction exitMainAction
private ShowActiveSettingsAction showActiveSettingsAction
private UnicodeToggleAction unicodeToggleAction
private final HidePackagePrefixToggleAction hidePackagePrefixToggleAction
private final TermLabelMenu termLabelMenu
javax.swing.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 javax.swing.JToolBar createFileOpsToolBar()
private javax.swing.JToolBar createProofControlToolBar()
private ComplexButton createSMTComponent()
private javax.swing.JComponent createWiderAutoModeButton()
protected MainStatusLine getStatusLine()
private void setStandardStatusLineImmediately()
public void setStandardStatusLine()
private void setStatusLineImmediately(java.lang.String str, int max)
public void setStatusLine(java.lang.String str, int max)
public void setStatusLine(java.lang.String s)
public void selectFirstTab()
public void freezeExceptAutoModeButton()
public void unfreezeExceptAutoModeButton()
public void makePrettyView()
private void addToProofList(ProofAggregate plist)
private javax.swing.JMenuBar createMenuBar()
private void createExtensionMenu(javax.swing.JMenuBar menuBar)
private javax.swing.JMenu createFileMenu()
private javax.swing.JMenu createViewMenu()
private javax.swing.JMenu createProofMenu()
private javax.swing.JMenu createOptionsMenu()
private javax.swing.JMenu createHelpMenu()
public void updateSMTSelectMenu()
private void updateDPSelectionMenu()
private MainWindow.SMTInvokeAction findAction(MainWindow.SMTInvokeAction[] actions, SolverTypeCollection union)
private void updateDPSelectionMenu(java.util.Collection<SolverTypeCollection> unions)
private javax.swing.JMenuItem setupSpeclangMenu()
public ProofTreeView getProofTreeView()
public CurrentGoalView getGoalView()
public void addProblem(ProofAggregate plist)
private void updateSequentView()
void displayResults(java.lang.String message)
public void notify(NotificationEvent event)
event
- the NotificationEventpublic void popupInformationMessage(java.lang.Object message, java.lang.String title)
public void popupWarning(java.lang.Object message, java.lang.String title)
public void popupInformationMessage(java.lang.Object message, java.lang.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 javax.swing.Action getOpenMostRecentFileAction()
public javax.swing.Action getUnicodeToggleAction()
public javax.swing.Action getHidePackagePrefixToggleAction()
public void savePreferences(java.awt.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(java.awt.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()
This is typically called at application termination.
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(java.lang.String absolutePath)
public void openExamples()
public void loadProblem(java.io.File file)
public void loadProblem(java.io.File file, java.util.List<java.io.File> classPath, java.io.File bootClassPath, java.util.List<java.io.File> includes)
public java.util.List<Name> getSortedTermLabelNames()
public javax.swing.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.public AutoModeAction getAutoModeAction()