edu.mit.csail.sdg.alloy4
Class Pos

java.lang.Object
  edu.mit.csail.sdg.alloy4.Pos

All Implemented Interfaces:

java.io.Serializable

public final class Pos
extends java.lang.Object
implements java.io.Serializable

Immutable; stores the filename and line/column position.

Invariant: filename!=null && x>0 && y>0 && ((y2>y && x2>0) || (y2==y && x2>=x))

Thread Safety: Safe (since objects of this class are immutable).

See Also:

Serialized Form

Field Summary

java.lang.String	filename The filename (it can be an empty string if unknown)
static Pos	UNKNOWN The default "unknown" location.
int	x The starting column position (from 1..)
int	x2 The ending column position (from 1..)
int	y The starting row position (from 1..)
int	y2 The ending row position (from 1..)

Constructor Summary

Pos(java.lang.String filename, int x, int y)
Constructs a new Pos object.

Pos(java.lang.String filename, int x, int y, int x2, int y2)
Constructs a new Pos object.

Method Summary

static boolean	before(Pos a, Pos b) Returns true if neither argument is null nor UNKNOWN, and that the ending position of "a" is before the starting position of "b".
boolean	equals(java.lang.Object other) Two Pos objects are equal if the filename x y x2 y2 are the same.
int	hashCode() Returns a hash code consistent with equals()
Pos	merge(Pos that) Return a new position that merges this and that (it is assumed that the two Pos objects have same filename)
java.lang.String	toShortString() Returns a short String representation of this position value.
java.lang.String	toString() Returns a String representation of this position value.

Methods inherited from class java.lang.Object

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

Field Detail

filename

public final java.lang.String filename

The filename (it can be an empty string if unknown)

x

public final int x

The starting column position (from 1..)

y

public final int y

The starting row position (from 1..)

x2

public final int x2

The ending column position (from 1..)

y2

public final int y2

The ending row position (from 1..)

UNKNOWN

public static final Pos UNKNOWN

The default "unknown" location.

Constructor Detail

Pos

public Pos(java.lang.String filename,
           int x,
           int y)

Constructs a new Pos object.

Parameters:

filename - - the filename (it can be an empty string if unknown)

x - - the column position (from 1..)

y - - the row position (from 1..)

Pos

public Pos(java.lang.String filename,
           int x,
           int y,
           int x2,
           int y2)

Constructs a new Pos object.

Parameters:

filename - - the filename (it can be an empty string if unknown)

x - - the starting column position (from 1..)

y - - the starting row position (from 1..)

x2 - - the ending column position (from 1..)

y2 - - the ending row position (from 1..)

Method Detail

merge

public Pos merge(Pos that)

Return a new position that merges this and that (it is assumed that the two Pos objects have same filename)

Parameters:

that - - the other position object

before

public static boolean before(Pos a,
                             Pos b)

Returns true if neither argument is null nor UNKNOWN, and that the ending position of "a" is before the starting position of "b".

equals

public boolean equals(java.lang.Object other)

Two Pos objects are equal if the filename x y x2 y2 are the same.

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Returns a hash code consistent with equals()

Overrides:

hashCode in class java.lang.Object

toShortString

public java.lang.String toShortString()

Returns a short String representation of this position value.

toString

public java.lang.String toString()

Returns a String representation of this position value.

Overrides:

toString in class java.lang.Object