001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java;
012:
013: /**
014: The position of a source element, given by its line and column
015: number.
016: Depending on the implementation, the valid range of defined line and
017: column numbers may be limited and cut off if superceded.
018: */
019:
020: public class Position {
021:
022: /**
023: The line number.
024: */
025:
026: private int line;
027:
028: /**
029: The column number.
030: */
031:
032: private int column;
033:
034: /**
035: The "undefined position" constant used to compare to undefined
036: positions or remove positional information.
037: */
038: public static final Position UNDEFINED = new Position();
039:
040: /**
041: Constructs a new invalid source code position object.
042: */
043: Position() {
044: line = column = -1;
045: }
046:
047: /**
048: Constructs a new source code position object.
049: @param line the line number.
050: @param column the column number.
051: */
052:
053: public Position(int line, int column) {
054: this .line = line;
055: this .column = column;
056: }
057:
058: /**
059: Returns the line number of this position.
060: @return the line number of this position.
061: */
062:
063: public int getLine() {
064: return line;
065: }
066:
067: /**
068: Returns the column number of this position.
069: @return the column number of this position.
070: */
071:
072: public int getColumn() {
073: return column;
074: }
075:
076: /**
077: Returns the hash code of this position.
078: @return the hash code of this position.
079: */
080:
081: public int hashCode() {
082: return column | (line << 8);
083: }
084:
085: /**
086: Compares this position with the given object for equality.
087: @return <CODE>true</CODE>, if the given object is a position
088: equals to this position, <CODE>false</CODE> otherwise.
089: */
090:
091: public boolean equals(Object x) {
092: if (x == this ) {
093: return true;
094: }
095: if (!(x instanceof Position)) {
096: return false;
097: }
098: Position p = (Position) x;
099: return line == p.line && column == p.column;
100: }
101:
102: /**
103: Compares this position with the given object for order.
104: An undefined position is less than any defined position.
105: @param x the position object to compare with.
106: @return a negative number, zero, or a positive number, if this
107: position is lower than, equals to, or higher than the given one.
108: */
109: public int compareTo(Object x) {
110: return compareTo((Position) x);
111: }
112:
113: /**
114: Compares this position with the given object for order.
115: An undefined position is less than any defined position.
116: @param p the position to compare with.
117: @return a negative number, zero, or a positive number, if this
118: position is lower than, equals to, or higher than the given one.
119: */
120: public int compareTo(Position p) {
121: return (line == p.line) ? (column - p.column) : (line - p.line);
122: }
123:
124: /**
125: Returns a string representation of this object.
126: */
127: public String toString() {
128: if (this != UNDEFINED) {
129: StringBuffer buf = new StringBuffer();
130: buf.append(line).append('/').append(column - 1);
131: return buf.toString();
132: } else {
133: return "??/??";
134: }
135: }
136:
137: }
|