| java.lang.Object
 de.uka.ilkd.key.pp.PosInSequent
| PosInSequent | | public class PosInSequent (Code) | | describes a position in a sequent including the bounds within a string
representation of the sequent. In contrast to PosInOccurrence and
PosInTerm of package de.uka.ilkd.key.logic, this class is mutable,
i.e the bounds may be set later in an already existing PosInSequent
instance. Apart from the bounds, PosInSequent has the following kind
of states: It marks the whole sequent, the whole antecedent, the whole
succedent or includes a PosInOccurrence if a position within a
constrained formula of the sequent is referred to. In the latter case
it contains also information whether the whole constrained formula
is referred to or the formula or the constraint.
|
| createCfmaPos | | public static PosInSequent createCfmaPos(PosInOccurrence posInOcc)(Code) | | creates a PosInSequent that points to a ConstrainedFormula described by
a PosInOccurrence. Additionally a boolean indicates whether the
the whole ConstrainedFormula or just the formula is meant.
Parameters:
posInOcc - the PositionInOccurrence describing theConstrainedFormula and maybe a subterm of its formula.
Parameters:
cfma - true iff the whole ConstrainedFormula (i.e. formula ANDconstraint) is meant. |
| createSequentPos | | public static PosInSequent createSequentPos()(Code) | | creates a PosInSequent that points to the whole sequent.
|
| getBounds | | public Range getBounds()(Code) | | returns the bounds in a string representation of a sequent
start position |
| getFirstJavaStatementRange | | public Range getFirstJavaStatementRange()(Code) | | returns the bounds, i.e. the start and end positions of the first Java statement,
of a corresponding Java program in a string representation of the sequent.
the range specifying the first statement in the corresponding program |
| getPosInOccurrence | | public PosInOccurrence getPosInOccurrence()(Code) | | returns the PosInOccurrence if the PosInSequent marks a
ConstrainedFormula or parts of it, null otherwise.
|
| isSequent | | public boolean isSequent()(Code) | | returns true if the PosInSequent points to a whole Sequent
|
| setBounds | | public void setBounds(Range r)(Code) | | sets the bounds, i.e. the start and end positions
of the PosInSequent
in a string representation of a sequent.
Parameters:
r - the range of character positions |
| setFirstJavaStatementRange | | public void setFirstJavaStatementRange(Range r)(Code) | | sets the bounds, i.e. the start and end positions of the first
Java statement, of a corresponding Java program in a string
representation of the sequent.
Parameters:
r - the range for the first statement in the corresponding program |
| toString | | public String toString()(Code) | | returns a string representation of this PosInSequent
|
|
|