javafe.util
Class FilterCorrelatedReader

java.lang.Object
  javafe.util.CorrelatedReader
      javafe.util.FilterCorrelatedReader

Direct Known Subclasses:

JmlCorrelatedReader

public class FilterCorrelatedReader

extends CorrelatedReader

This CorrelatedReader is built on top of another, given CorrelatedReader. All of the methods in this class simply call the corresponding methods on the underlying CorrelatedReader.

Author:

Rustan Leino

See Also:

CorrelatedReader

Field Summary

protected CorrelatedReader

child

Fields inherited from class javafe.util.CorrelatedReader

marked

Constructor Summary

protected

FilterCorrelatedReader(CorrelatedReader child) Constructs a FilterCorrelatedReader with child as the underlying CorrelatedReader.

Method Summary

void	clearMark() See documentation in superclass.
void	close() Closes us.
CorrelatedReader	createReaderFromMark(int discard) Creates a CorrelatedReader object for the input text from the marked position, to the current position.
GenericFile	getFile() Returns the file underlying this correlated reader.
int	getLocation() Returns the location of the last character read.
void	mark() See documentation in superclass.
int	read() Reads the next character from this input stream.
void	reset() See documentation in superclass.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

child

protected CorrelatedReader child

Constructor Detail

FilterCorrelatedReader

protected FilterCorrelatedReader(CorrelatedReader child)

Constructs a FilterCorrelatedReader with child as the underlying CorrelatedReader. After calling this constructor, the caller should no longer use child directly.

Method Detail

getFile

public GenericFile getFile()

Returns the file underlying this correlated reader.

Specified by:

getFile in class CorrelatedReader

getLocation

public int getLocation()

Returns the location of the last character read. If no character has been read yet, returns a whole-file location for this file.

Specified by:

getLocation in class CorrelatedReader

mark

public void mark()

See documentation in superclass.

Specified by:

mark in class CorrelatedReader

See Also:

CorrelatedReader.reset(), CorrelatedReader.clearMark(), CorrelatedReader.createReaderFromMark(int)

clearMark

public void clearMark()

See documentation in superclass.

Specified by:

clearMark in class CorrelatedReader

See Also:

CorrelatedReader.mark()

reset

public void reset()
           throws java.io.IOException

See documentation in superclass.

Specified by:

reset in class CorrelatedReader

Throws:

java.io.IOException - if this stream is not marked.

See Also:

CorrelatedReader.mark()

createReaderFromMark

public CorrelatedReader createReaderFromMark(int discard)
                                      throws java.lang.IndexOutOfBoundsException

Description copied from class: CorrelatedReader

Creates a CorrelatedReader object for the input text from the marked position, to the current position.

Calls to getLocation() for characters from the new CorrelatedReader yield the same locations as calls to getLocation() for the same characters on this CorrelatedReader.

The discard argument specifies the number of characters to discard from the end of the sub-CorrelatedReader.

Clears the mark as a side-effect.

Requires that the input stream had been previously marked via the mark() method and that we have not been closed.

Specified by:

createReaderFromMark in class CorrelatedReader

Throws:

java.lang.IndexOutOfBoundsException - if discard is negative or exceeds the number of marked characters

See Also:

BufferedCorrelatedReader.mark()

close

public void close()

Closes us. No other I/O operations may be called on us after we have been closed.

Overrides:

close in class CorrelatedReader

read

public int read()
         throws java.io.IOException

Reads the next character from this input stream. Does unicode conversion.

Requires we are open.

Specified by:

read in class CorrelatedReader

Returns:

A unicode character, or -1.

Throws:

java.io.IOException