    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.util;
    004
    005    import java.io.IOException;
    006    import javafe.genericfile.GenericFile;
    007
    008    /**
    009     * This CorrelatedReader is built on top of another, given CorrelatedReader.
    010     * All of the methods in this class simply call the corresponding methods
    011     * on the underlying CorrelatedReader.
    012     *
    013     * @see javafe.util.CorrelatedReader
    014     * @author Rustan Leino
    015     */
    016
    017    public class FilterCorrelatedReader extends CorrelatedReader
    018    {
    019        // Creation
    020
    021        protected /*@ non_null */ CorrelatedReader child;
    022
    023        /* The following invariant mentions "marked", which is not declared in
    024         * this class.  The justification for why it's still okay to declare
    025         * this invariant here is that all of the methods that modify "this.marked"
    026         * are overridden in the current class and, furthermore, the client is
    027         * not supposed to use "child" (hence, not "child.marked" either) after
    028         * passing it to the constructor.
    029         */
    030        //@ invariant marked == child.marked;
    031
    032        /** Constructs a FilterCorrelatedReader with <code>child</code> as the
    033         * underlying CorrelatedReader.  After calling this constructor, the
    034         * caller should no longer use <code>child</code> directly.
    035         */
    036
    037        protected FilterCorrelatedReader(/*@ non_null */ CorrelatedReader child) {
    038            child.clearMark();
    039            this.child = child;
    040        }
    041
    042        // Misc
    043
    044        /** Returns the file underlying this correlated reader.
    045         */
    046
    047        public GenericFile getFile() {
    048            return child.getFile();
    049        }
    050
    051
    052        // Getting Locations
    053
    054        /**
    055         * Returns the location of the last character read.  If no
    056         * character has been read yet, returns a whole-file location for
    057         * this file.
    058         */
    059
    060        public int getLocation() {
    061            return child.getLocation();
    062        }
    063
    064        // [Un]marking
    065
    066        /** See documentation in superclass.
    067         */
    068
    069        public void mark() {
    070            child.mark();
    071            marked = true;
    072        }
    073
    074        /** See documentation in superclass.
    075         */
    076
    077        public void clearMark() {
    078            child.clearMark();
    079            marked = false;
    080        }
    081
    082        /** See documentation in superclass.
    083         */
    084
    085        public void reset() throws IOException {
    086            child.reset();
    087            marked = false;
    088        }
    089
    090        public CorrelatedReader createReaderFromMark(int discard)
    091                throws IndexOutOfBoundsException {
    092            return child.createReaderFromMark(discard);
    093        }
    094
    095        // I/O
    096
    097        /**
    098         * Closes us.  No other I/O operations may be called on us after
    099         * we have been closed.
    100         */
    101
    102        public void close() {
    103            child.close();
    104            super.close();
    105        }
    106
    107        /**
    108         * Reads the next character from this input stream.
    109         * Does unicode conversion. <p>
    110         *
    111         *
    112         * Requires we are open.<p>
    113         *
    114         * @return   A unicode character, or -1.<p>
    115         */
    116        public int read() throws IOException {
    117            return child.read();
    118        }
    119    }