    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    }