See: Description
Interface | Description |
---|---|
SequentPrintFilterEntry |
One element of a sequent as delivered by SequentPrintFilter
|
VisibleTermLabels |
This abstract class is used by SequentViewLogicPrinter to determine the set
of printed TermLabels.
|
Class | Description |
---|---|
AbbrevMap | |
AbbrevMap.AbbrevWrapper | |
CharListNotation | |
HideSequentPrintFilter |
This filter takes a search string and yields a sequent containing only
sequent formulas that match the search.
|
IdentitySequentPrintFilter |
Identity Filter not doing anything
|
IdentitySequentPrintFilter.IdentityFilterEntry |
A filter entry, representing one sequent formula.
|
InitialPositionTable |
An InitialPositionTable is a PositionTable that describes the
beginning of the element/subelement relationship.
|
LogicPrinter |
The front end for the Sequent pretty-printer.
|
ModalityPositionTable |
This is a position table for program modality formulae.
|
Notation |
Encapsulate the concrete syntax used to print a term.
|
Notation.CastFunction |
The standard concrete syntax for casts.
|
Notation.Constant |
The standard concrete syntax for constants like true and false.
|
Notation.ElementaryUpdateNotation |
The standard concrete syntax for elementary updates.
|
Notation.ElementOfNotation |
The standard concrete syntax for the element of operator.
|
Notation.FunctionNotation |
The standard concrete syntax for function and predicate terms.
|
Notation.HeapConstructorNotation |
The standard concrete syntax for heap constructors.
|
Notation.IfThenElse |
The standard concrete syntax for conditional terms
if (phi) (t1) (t2) . |
Notation.Infix |
The standard concrete syntax for infix operators.
|
Notation.LabelNotation | |
Notation.ModalityNotation |
The standard concrete syntax for DL modalities box and diamond.
|
Notation.ModalSVNotation |
The concrete syntax for DL modalities represented with a
SchemaVariable.
|
Notation.ParallelUpdateNotation |
The standard concrete syntax for parallel updates
|
Notation.Postfix |
The standard concrete syntax for length.
|
Notation.Prefix |
The standard concrete syntax for prefix operators.
|
Notation.Quantifier |
The standard concrete syntax for quantifiers.
|
Notation.SchemaVariableNotation | |
Notation.SelectNotation |
The standard concrete syntax for select.
|
Notation.SeqConcatNotation | |
Notation.SeqGetNotation | |
Notation.SeqSingletonNotation |
The standard concrete syntax for sequence singletons.
|
Notation.SingletonNotation |
The standard concrete syntax for singleton sets.
|
Notation.StoreNotation |
The standard concrete syntax for store.
|
Notation.Subst |
The standard concrete syntax for substitution terms.
|
Notation.UpdateApplicationNotation |
The standard concrete syntax for update application.
|
Notation.VariableNotation |
The standard concrete syntax for all kinds of variables.
|
NotationInfo |
Stores the mapping from operators to
Notation s. |
PosInSequent |
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
PositionTable |
A PositionTable describes the start and end positions of substrings of a
String in order to get a PosInSequent from an int describing a position in a
string representing a Term or a Sequent, etc.
|
ProgramPrinter | |
Range |
A class specifying a range of integer numbers e.g.
|
RegroupSequentPrintFilter | |
SearchSequentPrintFilter |
This is an interface for filters that are used to
modify the sequent view, improving the search function.
|
SequentPrintFilter |
Filter a given sequent to prepare it for the SequentPrinter class
by adjusting constraints, deleting formulas, etc.
|
SequentViewLogicPrinter |
Subclass of
LogicPrinter used in GUI. |
ShowSelectedSequentPrintFilter |
This filter takes a
PosInOccurrence and only shows the sub-formula at that position. |
ShowSelectedSequentPrintFilter.Entry |
An Entry in
accessibility ShowSelectedSequentPrintFilter . |
Exception | Description |
---|---|
AbbrevException | |
IllegalRegexException |
This exception is thrown when a String is expected be a valid
regular expression, but is not.
|
Copyright © 2003-2019 The KeY-Project.