public class PositionTable
extends java.lang.Object
Positions are reckoned with start positions inclusive and end positions exclusive. Start and end positions are relative to each subterm.
Modifier and Type | Field and Description |
---|---|
protected PositionTable[] |
children
the PositionTables for the direct subterms (or parts of sequent, etc.)
|
protected int[] |
endPos |
protected int[] |
startPos |
Constructor and Description |
---|
PositionTable(int rows)
creates a new PositionTable with the number of subterms (or number of
SequentFormula in a Semisequent, or the number of Semisequents in a
Sequent, etc.)
|
Modifier and Type | Method and Description |
---|---|
Range |
firstStatementRangeForIndex(int index)
Returns the character range of the first java statement in a program
modality for the `lowest' subtable that includes
index in
its range. |
PositionTable |
getChild(int i)
Return of the children of this PositionTable
|
Range |
getFirstStatementRange() |
protected PosInSequent |
getSequentPIS(ImmutableList<java.lang.Integer> posList,
SequentPrintFilter filter)
Returns a PosInSequent for a given position list, but without filling in
the bounds.
|
protected ImmutableList<java.lang.Integer> |
pathForIndex(int index)
Returns the path to the `lowest' position table that includes
index in its range. |
Range |
rangeForIndex(int index,
int length)
Returns the character range of the `lowest' subtable that includes
index in its range. |
Range |
rangeForPath(ImmutableList<java.lang.Integer> path,
int length) |
void |
setEnd(int end,
PositionTable child)
sets end in the position table to the next free end entry in the position
table and sets the given PositionTable as child of the sub-element
finished by putting this end position
|
void |
setStart(int start)
Sets start in the position table for the next subterm to start.
|
void |
setStart(int subTermNo,
int start)
Sets start in the position table for the subterm with the given number to
start.
|
java.lang.String |
toString()
returns a String representation of the position table
|
protected int[] startPos
protected int[] endPos
protected PositionTable[] children
public PositionTable(int rows)
rows
- the number of direct sub-elements in the term whose position
information is represented by the constructed object.protected ImmutableList<java.lang.Integer> pathForIndex(int index)
index
in its range.public Range rangeForIndex(int index, int length)
index
in its range.index
- the character index to search for.length
- the length of the whole string corresponding to this position
table. Needed in case it turns out the index belongs to the
top level.index
in its range.public Range firstStatementRangeForIndex(int index)
index
in
its range. If the lowest subtable does not correspond to a program
modality, it returns null.public Range getFirstStatementRange()
ModalityPositionTable
.public Range rangeForPath(ImmutableList<java.lang.Integer> path, int length)
path
- the given integer list, i.e. pathlength
- length of the rangepublic void setEnd(int end, PositionTable child)
end
- char position that ends the sub-element started by the
corresponding start entry in the position tablechild
- PositionTable for the sub-element from start to endpublic void setStart(int start)
start
- char position that starts a sub-elementpublic void setStart(int subTermNo, int start)
subTermNo
- the 0-based number of the subterm to evaluatestart
- char position that starts a sub-elementpublic PositionTable getChild(int i)
public java.lang.String toString()
toString
in class java.lang.Object
protected PosInSequent getSequentPIS(ImmutableList<java.lang.Integer> posList, SequentPrintFilter filter)
posList
begins which the number of the formula. The returned
PosInSequent will refer to (a subterm of) one of the constrained formulae
in the sequent.posList
- the position list that navigates through the position tables.filter
- the sequent print filter from that was used to print the
sequentCopyright © 2003-2019 The KeY-Project.