Interface | Description |
---|---|
BuiltInRuleMenuItem | |
DragNDropInstantiator.TacletFilter |
This interface is impemented by filters selecting certain kinds of
taclets depending on their syntactic structure
|
HTMLSyntaxHighlighter.StringTransformer |
Simple interface as a replacement for a lambda realizing a String
transformation.
|
TacletMenuItem |
This interface is implemented by items to be displayed in
the @link TacletMenu.
|
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.
|
CurrentGoalViewListener |
reacts on mouse events to highlight the selected part of the sequent and it
pops up a menu showing all applicable Taclet at the highlighted position if
the mouse is pressed
Additionally it performs all necessary actions for draging some highlighted
sequent part into some other GUI component (e.g. some Taclet rule
instantiation dialog)
|
DefaultBuiltInRuleMenuItem |
equal to TacletMenuItem but for BuiltInRules
|
DefaultTacletMenuItem |
this class extends JMenuItem.
|
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 | |
InsertHiddenTacletMenuItem |
This item groups all insert hidden taclets and offers a
more convienient user interface to add them.
|
InsertionTacletBrowserMenuItem | |
InsertionTacletBrowserMenuItem.TacletAppListItem |
inner class to pretty print the formulas to be added
|
InsertSystemInvariantTacletMenuItem |
This menu item groups all taclets which allow to insert class invariants
|
InsertSystemInvariantTacletMenuItem.ClassInvAppItem |
inner class to pretty print the formulas to be added
|
InsertSystemInvariantTacletMenuItem.Lexicographical | |
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 | |
SequentViewChangeListener | |
SequentViewInputListener |
This class implements all input listener interfaces for SequentView.
|
SequentViewPanel |
Creates the layout for SequentViews.
|
SequentViewSearchBar | |
SimpleTacletSelectionMenu |
This simple taclet menu displays the user a list of applicable taclets
and lets select her/him one of those.
|
TacletDescriber |
The methods of class TacletDescriber have been extracted from class
InnerNodeView . |
TacletInfoToggle |
JCheckBox indicating whether taclet info is displayed for inner nodes
in proof tree. |
TacletMenu |
This class creates a menu with Taclets as entries.
|
TacletMenu.FocussedRuleApplicationMenuItem | |
TacletMenu.TacletAppComparator |
Enum | Description |
---|---|
SequentViewSearchBar.SearchMode |