|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjavafe.util.CorrelatedReader
javafe.util.BufferedCorrelatedReader
javafe.util.LocationManagerCorrelatedReader
This CorrelatedReader
class manages the allocation of
location numbers.
Field Summary | |
private static java.util.Vector |
allCorrStreams
A static Vector containing all LocationManagerCorrelatedReader instances, in the order they were allocated, which is used to map a given location to a corresponding LocationManagerCorrelatedReader instance. |
protected int |
curLineNo
The current line number; that is, the number of |
private static int |
freeLoc
The next location to be allocated to a LocationManagerCorrelatedReader instance. |
protected boolean |
isWholeFile
Are all of our locations whole-file locations? |
private int |
markLineNo
The value of curLineNo at the mark point (if marked is true). |
(package private) static int |
MAXFILESIZE
A location is an integer that encodes file/line/column/offset information. |
private int[] |
NLOA
Each LocationManagerCorrelatedReader has a "new line offset array", or NLOA, that contains the offset of the beginning of each line. |
private static int |
NLOA_DEFAULT_SIZE
The default initial size to allocate an NLOA array |
protected int |
streamid
|
static int |
totalLinesRead
The total # of lines that have been read so far by all FileCorrelatedReaders. |
Fields inherited from class javafe.util.BufferedCorrelatedReader |
beforeBufLoc, buf, curNdx, endBufNdx, lastCharNdx, markNdx, maxLoc, minLoc, oddSlashLoc, STARTFREELOC |
Fields inherited from class javafe.util.CorrelatedReader |
marked |
Constructor Summary | |
(package private) |
LocationManagerCorrelatedReader()
This constructor allocates a range of location for use by the CorrelatedReader. |
Method Summary | |
static void |
clear()
|
void |
close()
Closes us. |
static java.util.Vector |
fileNumbersToNames()
Creates and returns a vector that associates file numbers to file names. |
protected static LocationManagerCorrelatedReader |
getCorrStreamAt(int i)
Return the LocationManagerCorrelatedReader associated with streamId i. |
(package private) static boolean |
isWholeFileLoc(int loc)
Is a location a whole file location? |
private static int |
locToColOrLine(int loc,
boolean wantColumn)
Returns the column number (if wantColumn) or line number (if ! |
(package private) static int |
locToColumn(int loc)
Returns the column number associated with location loc . |
(package private) static GenericFile |
locToFile(int loc)
Returns the GenericFile associated with location loc . |
(package private) static int |
locToLineNumber(int loc)
Returns the line number associated with location loc . |
(package private) static int |
locToOffset(int loc)
Returns the offset associated with location loc . |
protected static LocationManagerCorrelatedReader |
locToStream(int loc)
Return the LocationManager CorrelatedReader instance associated with location loc. |
(package private) static int |
locToStreamId(int loc)
Returns the internal stream ID used for the stream associated with location loc .
|
(package private) static int |
makeLocation(int streamId,
int line,
int col)
Attempt to return the valid regular location associated with a given streamId, line #, and col #. |
void |
mark()
Marks the position of the current character in this input stream. |
protected void |
recordNewLineLocation()
Records a newline at the current location. |
void |
reset()
Repositions this stream to the position at the time the mark method was last called on this input stream. |
(package private) static GenericFile |
streamIdToFile(int id)
Returns the GenericFile associated with stream id id , where id has previously been
returned by locToStreamId .
|
java.lang.String |
toString()
|
Methods inherited from class javafe.util.BufferedCorrelatedReader |
clearMark, createReaderFromMark, getBeforeMarkLocation, getBufferFromMark, getLocation, peek, readRaw, refillBuf |
Methods inherited from class javafe.util.CorrelatedReader |
getFile, read |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Field Detail |
private static int freeLoc
We do not use ints below STARTFREELOC to denote locations. If freeLoc+MAXFILESIZE results in an overflow, then too many LocationManagerCorrelatedReader instances have been created and an assertion failure occurs.
static final int MAXFILESIZE
private int[] NLOA
NLOA is defined for indexes in [0..curLineNo).
If NLOA[i], i in [0..curLineNo), = j, then the characters at offset j and j-1 were on different lines. Furthermore, either (a) i=j=0, or (b) i>0, j>0, and the character at offset j-1 is a newline.
Note: this means a line ends just *after* a newline, not before.
private static final int NLOA_DEFAULT_SIZE
protected int streamid
private static java.util.Vector allCorrStreams
A location's streamId is its index in allCorrStreams. See locToStreamId(int) for the algorithm mapping locations to streamId's.
protected boolean isWholeFile
public static int totalLinesRead
This is not used internally, and is kept only for interested clients.
protected int curLineNo
(Line numbers are counted from 1 not 0.)
private int markLineNo
The justification for why it's okay to place the following invariant
in this class, even though marked
is declared in the
superclass, is that this class overrides the methods that set
marked
to true
. (But there's no mechanical
check that this justification is upheld, so it needs to be upheld
manually.)
Constructor Detail |
LocationManagerCorrelatedReader()
Method Detail |
public void close()
close
in class BufferedCorrelatedReader
protected void recordNewLineLocation()
public static java.util.Vector fileNumbersToNames()
protected static LocationManagerCorrelatedReader getCorrStreamAt(int i)
If i is not a valid streamId (aka, i not in [0, allCorrStreams.size()) ), an assertion failure occurs.
static int makeLocation(int streamId, int line, int col)
If there is no such location currently in existence, an assertion failure will occur.
This method is intended mainly for debugging purposes.
protected static LocationManagerCorrelatedReader locToStream(int loc)
Requires that loc be a valid location.
static int locToStreamId(int loc)
loc
.
Requires that loc be a valid location.
static boolean isWholeFileLoc(int loc)
static int locToOffset(int loc)
loc
. Requires that loc be a valid regular location (regular ==> not a whole-file location).
Note: offsets start with 1 (a la emacs).
static int locToLineNumber(int loc)
loc
. Requires that loc be a valid regular location (regular ==> not a whole-file location).
Note: line numbers start with 1 (a la emacs).
static int locToColumn(int loc)
loc
. Requires that loc be a valid regular location (regular ==> not a whole-file location).
Note: column numbers start with 0.
private static int locToColOrLine(int loc, boolean wantColumn)
loc
. Requires that loc be a valid regular location (regular ==> not a whole-file location).
Note: line numbers start with 1 (a la emacs), while column numbers start with 0.
static GenericFile streamIdToFile(int id)
id
, where id
has previously been
returned by locToStreamId
.
Requires that id be a valid streamId.
static GenericFile locToFile(int loc)
loc
. Requires that id be a valid streamId of a FileCorrelatedReader.
public void mark()
BufferedCorrelatedReader
reset
method
repositions this stream at the last marked position.
This method differs from
java.io.InputStream.readlimit
in that it does not
take a readlimit
argument.
mark
in class BufferedCorrelatedReader
BufferedCorrelatedReader.reset()
,
BufferedCorrelatedReader.clearMark()
,
BufferedCorrelatedReader.createReaderFromMark(int)
public void reset() throws java.io.IOException
BufferedCorrelatedReader
mark
method was last called on this input stream.
Requires that the input stream had been previously marked
via the mark()
method.
If mark() is called before read(), then the mark will be restored to its previous value (and not the preceeding character().
reset
in class BufferedCorrelatedReader
java.io.IOException
- if this stream is not marked.BufferedCorrelatedReader.mark()
public java.lang.String toString()
public static void clear()
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |