de.uka.ilkd.key.java

Class Position

java.lang.Object

de.uka.ilkd.key.java.Position

public class Position
extends java.lang.Object

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

Fields

Modifier and Type	Field and Description
private int	column The column number.
private int	line The line number.
static Position	UNDEFINED The "undefined position" constant used to compare to undefined positions or remove positional information.

Constructor Summary

Constructors

Constructor and Description
Position() Constructs a new invalid source code position object.
Position(int line, int column) Constructs a new source code position object.

Method Summary

Modifier and Type	Method and Description
int	compareTo(java.lang.Object x) Compares this position with the given object for order.
int	compareTo(Position p) Compares this position with the given object for order.
boolean	equals(java.lang.Object x) Compares this position with the given object for equality.
int	getColumn() Returns the column number of this position.
int	getLine() Returns the line number of this position.
int	hashCode() Returns the hash code of this position.
boolean	isNegative() Helper method for validity checks.
java.lang.String	toString() Returns a string representation of this object.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

line

private final int line

The line number.

column

private final int column

The column number.

UNDEFINED

public static final Position UNDEFINED

The "undefined position" constant used to compare to undefined positions or remove positional information.

Constructor Detail

Position

Position()

Constructs a new invalid source code position object.

Position

public Position(int line,
                int column)

Constructs a new source code position object.

Parameters:

line - the line number.

column - the column number.

Method Detail

getLine

public int getLine()

Returns the line number of this position.

Returns:

the line number of this position.

getColumn

public int getColumn()

Returns the column number of this position.

Returns:

the column number of this position.

hashCode

public int hashCode()

Returns the hash code of this position.

Overrides:

hashCode in class java.lang.Object

Returns:

the hash code of this position.

equals

public boolean equals(java.lang.Object x)

Compares this position with the given object for equality.

Overrides:

equals in class java.lang.Object

Returns:

true, if the given object is a position equals to this position, false otherwise.

compareTo

public int compareTo(java.lang.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.

Returns:

a negative number, zero, or a positive number, if this position is lower than, equals to, or higher than the given one.

compareTo

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.

Returns:

a negative number, zero, or a positive number, if this position is lower than, equals to, or higher than the given one.

isNegative

public boolean isNegative()

Helper method for validity checks.

Returns:

true iff either line or column are negative

toString

public java.lang.String toString()

Returns a string representation of this object.

Overrides:

toString in class java.lang.Object