See: Description
| Interface | Description |
|---|---|
| GUIListener |
GUIListener defines the interface for an object that listens to
actions of gui components, e.g. it is informed if a gui component
requests modal access.
|
| InteractiveRuleApplicationCompletion |
Instances of class implementing this interface are able to complete rule applications.
|
| KeYListener |
KeYListener is used for global changes that might affect most of
all KeY-Components.
|
| TacletMatchCompletionDialog.PositionSettable |
| Class | Description |
|---|---|
| ApplyTacletDialog | |
| AutoDismissDialog | |
| AuxiliaryContractConfigurator<T extends AuxiliaryContract> |
A window to contain a
AuxiliaryContractSelectionPanel. |
| AuxiliaryContractSelectionPanel<T extends AuxiliaryContract> |
This panel used to select which
T(s) to use for a
AbstractAuxiliaryContractRule. |
| BlockContractExternalCompletion |
Interactive completion for
BlockContractExternalBuiltInRuleApp. |
| BlockContractInternalCompletion |
Interactive completion of
BlockContractInternalBuiltInRuleApp. |
| BlockContractSelectionPanel |
This panel used to select which
BlockContracts to use for an
AbstractBlockContractBuiltInRuleApp. |
| ClassSelectionDialog |
A dialog for selecting classes (including interfaces).
|
| ClassSelectionDialog.WrappedKJT | |
| ClassTree | |
| ClassTree.Entry | |
| ContractConfigurator | |
| ContractSelectionPanel |
A panel for selecting contracts.
|
| DependencyContractCompletion |
This class completes the instantiation for a dependency contract
applications.
|
| DependencyContractCompletion.TermStringWrapper | |
| ExampleChooser | |
| ExampleChooser.Example |
This class wraps a
File and has a special ExampleChooser.Example.toString() method
only using the short file name w/o path. |
| ExceptionalHandler |
This is a handy class for tracing Exceptions that are otherwise lost in
the thread chaos.
|
| ExceptionDialog |
Dialog to display error messages.
|
| FunctionalOperationContractCompletion |
This class completes the instantiation for a functional operation contract
applications.
|
| GoalList | |
| GoalList.GoalListModel | |
| HeatmapOptionsDialog |
This Dialog contains options for highlighting sequent formulae or terms
according to their age, i.e., when they were first introduced into the proof.
|
| IconFactory | |
| IconFactory.KeYControlIcon | |
| IconFactory.KeYFolderIcon | |
| InfoTree |
This class is used by
InfoView to display its contents. |
| InfoTreeModel |
Extension of
DefaultTreeModel used by InfoTree. |
| InfoTreeNode |
Every node of
InfoTree is an instance of this class. |
| InfoView |
Class for info contents displayed in
MainWindow. |
| InfoViewContentPane |
This class is used to display descriptions in
InfoView. |
| InspectorForDecisionPredicates | |
| InvariantConfigurator | |
| KeYFileChooser | |
| LoopApplyHeadCompletion |
Interactive completion for
LoopApplyHeadBuiltInRuleApp. |
| LoopContractExternalCompletion |
Interactive completion for
LoopContractExternalBuiltInRuleApp. |
| LoopContractInternalCompletion |
Interactive completion for
LoopContractInternalBuiltInRuleApp. |
| LoopContractSelectionPanel |
This panel used to select which
LoopContracts to use for an
AbstractLoopContractBuiltInRuleApp. |
| LoopInvariantRuleCompletion |
This class completes the instantiations of the loop invariant rule
applications.
|
| MainStatusLine | |
| MainWindow | |
| 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
|
| 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
|
| MainWindowTabbedPane | |
| Markdown |
A facade to the world of Markdown.
|
| MaxRuleAppSlider | |
| ProofMacroMenu |
This class provides the user interface to the macro extensions.
|
| ProofMacroWorker |
The Class ProofMacroWorker is a swing worker for the application of proof
macros.
|
| ProofManagementDialog | |
| ProofManagementDialog.ProofWrapper | |
| ProofScriptWorker | |
| RecentFileMenu |
This class offers a mechanism to manage recent files; it adds the
necessary menu items to a menu or even can provide that menu itself.
|
| RecentFileMenu.RecentFileEntry | |
| SearchBar | |
| StrategySelectionView | |
| StrategySelectionView.StrategySelectionComponents |
Provided via
StrategySelectionView#getStrategySelectionComponents() for direct
access to created user interface components. |
| TableRowResizer |
A mouse listener for resizing the height of the JTable rows.
|
| TacletIfSelectionDialog |
this dialog appears if a rule is selected to be applied and the rule has an
if sequent.
|
| TacletIfSelectionDialog.IfComboRenderer | |
| TacletMatchCompletionDialog | |
| TacletMatchCompletionDialog.DataTable | |
| TaskTree | |
| TaskTree.TaskTreeIconCellRenderer | |
| WindowUserInterfaceControl |
Implementation of
UserInterfaceControl which controls the MainWindow
with the typical user interface of KeY. |