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    }