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

javafe.util
Class FilterCorrelatedReader

java.lang.Object
  extended byjavafe.util.CorrelatedReader
      extended byjavafe.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

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

The ESC/Java2 Project Homepage