Interface | Description |
---|---|
BuiltInRuleMenuItem | |
DragNDropInstantiator.TacletFilter |
This interface is impemented by filters selecting certain kinds of
taclets depending on their syntactic structure
|
Class | Description |
---|---|
CurrentGoalView |
This sequent view displays the sequent of an open goal and allows selection
of formulas as well as the application of rules.
|
CurrentGoalViewMenu |
The menu shown by a
CurrentGoalViewListener when the user clicks on a
CurrentGoalView . |
CurrentGoalViewMenu.TacletAppComparator | |
DragNDropInstantiator |
The DragNDropInstantiator interpretes drag'n drop actions as taclet
instantiations.
|
DragNDropInstantiator.TacletFilter.TacletWithIfFindAndNoReplacewith |
This filter selects all Taclet which have an assumes,
find and no replacewith part.
|
DragNDropInstantiator.TacletFilter.TacletWithIfFindAndReplacewith |
This filter selects all Taclet which have an assumes,
find and at least one replacewith part.
|
DragNDropInstantiator.TacletFilter.TacletWithNoIf |
This filter selects all Taclet which have no assume, but a
find.
|
DragNDropInstantiator.TacletFilter.TacletWithNoIfFindAndAddrule |
This filter selects all Taclet which have no assumes, but a
find and at least one addrule section.
|
EmptySequent |
Use this class in case no proof is loaded.
|
HTMLSyntaxHighlighter |
Performs a simple pattern-based syntax highlighting for KeY sequents by
adding styled HTML tags.
|
InnerNodeView |
Sequent view for an inner node.
|
InnerNodeViewListener |
Listener for an
InnerNodeView
Reacts on mouse events to highlight the selected part of the sequent and it
pops up a menu showing all applicable actions at the highlighted position. |
InnerNodeViewMenu |
The menu shown by a
InnerNodeViewListener
when the user clicks on an InnerNodeView . |
InsertHiddenTacletMenuItem |
This item groups all insert hidden taclets and offers a
more convienient user interface to add them.
|
InsertionTacletBrowserMenuItem | |
InsertSystemInvariantTacletMenuItem |
This menu item groups all taclets which allow to insert class invariants
|
MainFrame |
Central part of MainWindow.
|
MenuItemForTwoModeRules | |
PosInSequentTransferable |
This class in an implementation of the
Transferable interface and
allows to transfer a PosInSequent object. |
SequentHideWarningBorder |
A special purpose border that prints a warning window if the search bar
filtering removes formulas from the display.
|
SequentView | |
SequentViewDock | |
SequentViewDock.OpenCurrentNodeAction | |
SequentViewInputListener |
This class implements all input listener interfaces for SequentView.
|
SequentViewMenu<T extends SequentView> |
The menu shown by a
SequentViewListener when the user clicks on a SequentView . |
SequentViewSearchBar | |
ShowHashcodesExtension |
Extension adapter for showing hash codes for terms.
|
SimpleTacletSelectionMenu |
This simple taclet menu displays the user a list of applicable taclets
and lets select her/him one of those.
|
TacletInfoToggle |
JCheckBox indicating whether taclet info is displayed for inner nodes
in proof tree. |
Enum | Description |
---|---|
SequentViewSearchBar.SearchMode |
Copyright © 2003-2019 The KeY-Project.