public class PositionInfo
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static PositionInfo |
UNDEFINED
PositionInfo with undefined positions.
|
static java.net.URI |
UNKNOWN_URI
Unknown URI (enables us to always have a non-null value for fileURI)
|
Constructor and Description |
---|
PositionInfo(Position relPos,
Position startPos,
Position endPos)
Creates a new PositionInfo without resource information but only with positions.
|
PositionInfo(Position relPos,
Position startPos,
Position endPos,
java.net.URI fileURI)
Creates a new PositionInfo without the given resource information.
|
Modifier and Type | Method and Description |
---|---|
Position |
getEndPosition() |
java.lang.String |
getFileName()
Deprecated.
This method should no longer be used, as PositionInfo can now be used with
resources other than files. Use
getURI() instead. |
java.lang.String |
getParentClass()
Deprecated.
This method should no longer be used, as PositionInfo can now be used with
resources other than files. Use
getParentClassURI() instead. |
java.net.URI |
getParentClassURI() |
Position |
getRelativePosition() |
Position |
getStartPosition() |
java.net.URI |
getURI() |
static PositionInfo |
join(PositionInfo p1,
PositionInfo p2)
Creates a new PositionInfo from joining the intervals of the given PositionInfos.
|
boolean |
startEndValid()
Checks if start and end position are both defined and in valid range.
|
java.lang.String |
toString() |
public static final java.net.URI UNKNOWN_URI
public static final PositionInfo UNDEFINED
public PositionInfo(Position relPos, Position startPos, Position endPos)
relPos
- the relative positionstartPos
- the start positionendPos
- the end positionpublic PositionInfo(Position relPos, Position startPos, Position endPos, java.net.URI fileURI)
relPos
- the relative positionstartPos
- the start positionendPos
- the end positionfileURI
- the resource the PositionInfo refers to@Deprecated public java.lang.String getParentClass()
getParentClassURI()
instead.@Deprecated public java.lang.String getFileName()
getURI()
instead.public java.net.URI getParentClassURI()
public java.net.URI getURI()
public Position getRelativePosition()
public Position getStartPosition()
public Position getEndPosition()
public static PositionInfo join(PositionInfo p1, PositionInfo p2)
p1
- the first PositionInfop2
- the second PositionInfopublic boolean startEndValid()
public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.