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 }