001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.util;
004    
005    import java.io.*; 
006    
007    import javafe.genericfile.GenericFile;
008    
009    /** 
010     * A reader (aka input stream) that provides an associated
011     * <I>location</I> with each character read.
012     *
013     * <p> See javafe.util.Location for the interpretation of these locations.
014     *
015     * <p> This class also takes care of unicode conversion.  A unicode
016     * character sequence consists of a backslash that is preceded by an
017     * even number of backslashes, followed by one or more 'u's, followed
018     * by four hexadecimal digits. This class converts each unicode character
019     * sequence into a single character.
020     *
021     * <p> This class also provides the ability to mark a specific point
022     * in the input stream, and to reposition the stream at the marked
023     * position. We also provide a method to create a new
024     * <code>CorrelatedReader</code> for the text between the marked
025     * position and the current point in the stream. Marking is also
026     * allowed on the new <code>CorrelatedReader</code> object. For
027     * efficiency, we also provide the facility to remove the mark from
028     * the stream.<p>
029     *
030     * @see javafe.util.Location
031     * @author Cormac Flanagan
032     */
033    
034    public abstract class CorrelatedReader 
035    /* may later want "extends Reader" */
036    {
037        // Creation
038    
039        /** Simple constructor.  Pretty boring, really. */
040        //@ ensures !marked;
041    
042        protected CorrelatedReader() {}
043    
044        // Misc
045    
046        /** Returns the file underlying this correlated reader. */
047        //@ ensures \result != null;
048    
049        public abstract GenericFile getFile();
050    
051        // Getting Locations
052    
053        /**
054         * Returns the location of the last character read.  If no
055         * character has been read yet, returns a whole-file location for
056         * this file.
057         */
058        //@ ensures \result != Location.NULL;
059    
060        public abstract int getLocation();
061    
062        // [Un]marking
063    
064        /**
065         * True iff a mark has been set.
066         */
067    
068        /*@ spec_public */ protected boolean marked = false;
069    
070        /**
071         * Marks the position of the current character in this input
072         * stream.  A subsequent call to the <code>reset</code> method
073         * repositions this stream at the last marked position. <p>
074         *
075         * This method differs from
076         * <code>java.io.InputStream.readlimit</code> in that it does not
077         * take a <code>readlimit</code> argument. <p>
078         *
079         * @see javafe.util.CorrelatedReader#reset()
080         * @see javafe.util.CorrelatedReader#clearMark()
081         * @see javafe.util.CorrelatedReader#createReaderFromMark
082         */
083        //-@ modifies marked;
084        //@ ensures marked;
085    
086        public abstract void mark();
087    
088        /**
089         * Removes the mark (if any) from the input stream.
090         *
091         * @see javafe.util.CorrelatedReader#mark()
092         */
093        //@ modifies marked;
094        //@ ensures !marked;
095    
096        public abstract void clearMark();
097    
098        /**
099         * Repositions this stream to the position at the time the
100         * <code>mark</code> method was last called on this input stream. <p>
101         *
102         * Requires that the input stream had been previously marked 
103         * via the <code>mark()</code> method. <p>
104         *
105         * If mark() is called before read(), then the mark will be
106         * restored to its previous value (and not the preceeding
107         * character().<p>
108         *
109         * @exception IOException  if this stream is not marked.
110         * @see javafe.util.CorrelatedReader#mark()
111         */
112        //@ requires marked;
113        //-@ modifies marked;
114        //@ ensures !marked;
115    
116        public abstract void reset() throws IOException;
117    
118        /**
119         * Creates a <code>CorrelatedReader</code> object for the input
120         * text from the marked position, to the current position. <p>
121         *
122         * Calls to <code>getLocation()</code> for characters from the
123         * new <code>CorrelatedReader</code> yield the same locations as
124         * calls to <code>getLocation()</code> for the same characters on
125         * this <code>CorrelatedReader</code>. <p>
126         *
127         * The <code>discard</code> argument specifies the number of
128         * characters to discard from the end of the
129         * sub-<code>CorrelatedReader</code>. <p>
130         *
131         * Clears the mark as a side-effect. <p>
132         *
133         * Requires that the input stream had been previously marked via
134         * the <code>mark()</code> method and that we have not been
135         * closed. <p>
136         *
137         * @exception IndexOutOfBoundsException if <code>discard</code> is
138         * negative or exceeds the number of marked characters
139         *
140         * @see javafe.util.BufferedCorrelatedReader#mark()
141         */
142        //@ requires 0 <= discard;
143        //@ requires marked;
144        //@ modifies marked;
145        //@ ensures \result != null;
146        //@ ensures !marked;
147    
148        public abstract CorrelatedReader createReaderFromMark(int discard)
149                throws IndexOutOfBoundsException;
150    
151        // I/O
152    
153        /**
154         * Closes us.  No other I/O operations may be called on us after
155         * we have been closed.
156         */
157    
158        public void close() {}
159    
160        /**
161         * Reads the next character from this input stream.  Does unicode
162         * conversion. <p>
163         *
164         * Requires we are open.<p>
165         * 
166         * @return A unicode character, or -1.<p>
167         */
168        public abstract int read() throws IOException;
169    }