| java.lang.Object
 de.uka.ilkd.key.java.Position
| Position | | public class Position (Code) | | The position of a source element, given by its line and column
number.
Depending on the implementation, the valid range of defined line and
column numbers may be limited and cut off if superceded.
|
| Field Summary | |
| final public static Position | UNDEFINED
The "undefined position" constant used to compare to undefined
positions or remove positional information. |
| Constructor Summary | |
| | Position()
Constructs a new invalid source code position object. | | public | Position(int line, int column)
Constructs a new source code position object. |
| Method Summary | |
| public int | compareTo(Object x)
Compares this position with the given object for order.
An undefined position is less than any defined position.
Parameters:
x - the position object to compare with. | | public int | compareTo(Position p)
Compares this position with the given object for order.
An undefined position is less than any defined position.
Parameters:
p - the position to compare with. | | public boolean | equals(Object x)
Compares this position with the given object for equality. | | public int | getColumn()
Returns the column number of this position. | | public int | getLine()
Returns the line number of this position. | | public int | hashCode()
Returns the hash code of this position. | | public String | toString()
Returns a string representation of this object. |
| UNDEFINED | | final public static Position UNDEFINED(Code) | | The "undefined position" constant used to compare to undefined
positions or remove positional information.
|
| Position | | Position()(Code) | | Constructs a new invalid source code position object.
|
| Position | | public Position(int line, int column)(Code) | | Constructs a new source code position object.
Parameters:
line - the line number.
Parameters:
column - the column number. |
| compareTo | | public int compareTo(Object x)(Code) | | Compares this position with the given object for order.
An undefined position is less than any defined position.
Parameters:
x - the position object to compare with. a negative number, zero, or a positive number, if thisposition is lower than, equals to, or higher than the given one. |
| compareTo | | public int compareTo(Position p)(Code) | | Compares this position with the given object for order.
An undefined position is less than any defined position.
Parameters:
p - the position to compare with. a negative number, zero, or a positive number, if thisposition is lower than, equals to, or higher than the given one. |
| equals | | public boolean equals(Object x)(Code) | | Compares this position with the given object for equality.
true, if the given object is a positionequals to this position, false otherwise. |
| getColumn | | public int getColumn()(Code) | | Returns the column number of this position.
the column number of this position. |
| getLine | | public int getLine()(Code) | | Returns the line number of this position.
the line number of this position. |
| hashCode | | public int hashCode()(Code) | | Returns the hash code of this position.
the hash code of this position. |
| toString | | public String toString()(Code) | | Returns a string representation of this object.
|
|
|