001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package javafe.util;
004
005 import java.io.*;
006
007 import javafe.genericfile.*;
008 import javafe.util.Assert;
009
010 /**
011 * A <code>FileCorrelatedReader</code> is a
012 * <code>CorrelatedReader</code> that reads its characters from a
013 * stream that corresponds to a file.
014 *
015 * <p> The class also provides a method to create a new
016 * <code>CorrelatedReader</code> for the text between the marked
017 * position and the current point in the stream.
018 *
019 * @see javafe.util.Location
020 * @author Cormac Flanagan, Rustan Leino
021 */
022
023 public class FileCorrelatedReader extends LocationManagerCorrelatedReader
024 {
025 // Class variables & constants
026
027 /** How big a block to read from a stream at a time */
028
029 private static final int READBLOCKSIZE = 256;
030
031 /** The initial size for buf */
032
033 private static final int DEFAULTBUFSIZE = READBLOCKSIZE;
034
035 // Instance variables
036
037 /**
038 * The stream for this CorrelatedReader if it is open and not a
039 * subReader. Null otherwise.
040 *
041 * (A CorrelatedReader is defined to be open iff buf is non-null.)
042 */
043 //@ invariant (buf != null) == (stream != null);
044
045 //@ spec_public
046 private InputStream stream;
047
048 /**
049 * The GenericFile for this CorrelatedReader.
050 */
051
052 private /*@ non_null @*/ GenericFile file;
053
054 // Creation
055
056 /**
057 * Constructs a correlated input stream that reads its input from
058 * the specified GenericFile.
059 */
060 public FileCorrelatedReader(/*@ non_null @*/ GenericFile file)
061 throws java.io.IOException {
062 this(file.getInputStream(), file);
063 }
064
065 /**
066 * This is a specialized constructor used for InputStreams that
067 * are not reopenable such as stdin.<p>
068 *
069 * streamName is the human readable name of the stream.
070 */
071 public FileCorrelatedReader(/*@ non_null @*/ InputStream in,
072 /*@ non_null @*/ String streamName) {
073 this(in, new UnopenableFile(streamName));
074 }
075
076 /**
077 * Constructs a correlated input stream that reads its input from
078 * the specified input stream.
079 *
080 * file is an associated GenericFile that may be used to reopen
081 * the specified input stream
082 */
083
084 private FileCorrelatedReader(/*@ non_null @*/ InputStream in,
085 /*@ non_null @*/ GenericFile file) {
086 super(); // allocate location numbers, etc.
087
088 this.stream = in;
089 this.file = file;
090
091 this.buf = new byte[DEFAULTBUFSIZE];
092 this.endBufNdx = 0;
093 //System.out.println("NEW STREAM " + streamid + " " + file.getHumanName());
094 }
095
096 /**
097 * Create a whole file location for a given GenericFile. <p>
098 *
099 * file need not be openable.
100 */
101 //@ ensures \result != Location.NULL;
102
103 static int createWholeFileLoc(/*@ non_null @*/ GenericFile file) {
104 // TBW: This implementation leaves something to be desired. It would be
105 // nice if whole-file correlated readers could be their own subclass of
106 // LocationManagerCorrelatedReader.
107 try {
108 /*
109 * Create a CorrelatedReader for file, but substituting
110 * a dummy InputStream instead of reading from file.
111 * (file may not be openable.)
112 */
113 FileCorrelatedReader R =
114 new FileCorrelatedReader(new ByteArrayInputStream(new byte[10]), file);
115
116 // Then read the first character so it has a valid location:
117 R.read();
118
119 // Close it and turn it into a whole file CorrelatedReader:
120 R.close();
121 R.isWholeFile = true;
122
123 // Finally, return its location:
124 return R.getLocation();
125
126 } catch (IOException e) {
127 Assert.fail("I/O error reading from a ByteArrayInputStream");
128 return Location.NULL; // dummy return...
129 }
130 }
131
132 /**
133 * Closes us. No other I/O operations may be called on us after
134 * we have been closed.
135 */
136 //@ also modifies stream;
137
138 public void close() {
139 super.close();
140 if (stream != null) {
141 try {
142 stream.close();
143 } catch (IOException e) {
144 // skip
145 }
146 stream = null;
147 }
148 }
149
150 // The methods
151
152 /** See spec in the abstract <code>CorrelatedReader</code> class.
153 */
154
155 public int read() throws IOException {
156 if (buf == null) {
157 Assert.precondition("read() called on a closed CorrelatedReader");
158 }
159
160 if (curNdx == endBufNdx) {
161 // refill buffer
162 if (!refillBuf()) {
163 // EOF
164 // save position of last character
165 lastCharNdx = curNdx;
166 return -1;
167 }
168 }
169
170 // save the position of this character, before it is read:
171 lastCharNdx = curNdx;
172
173 int c = buf[curNdx++];
174
175 if (c=='\\' && oddSlashLoc+1 != getLocation()) {
176 // Can be a unicode escape sequence (is an odd slash!)
177 if (peek() == 'u') {
178 // is a unicode escape sequence
179 while (peek() == 'u') {
180 curNdx++;
181 }
182 char s[] = new char[4];
183 for (int i=0; i<4; i++) {
184 s[i] = (char)readRaw();
185 if (Character.digit(s[i],16)==-1)
186 throw new IOException("Bad unicode character sequence");
187 }
188 c = Integer.parseInt( new String(s), 16 );
189 } else {
190 // not a unicode
191 oddSlashLoc = getLocation();
192 }
193 } else if (c=='\n') {
194 recordNewLineLocation();
195 totalLinesRead++;
196 curLineNo++;
197 }
198
199 return c;
200 }
201
202 /**
203 * Refills the buffer. <p>
204 *
205 * If the mark is set, and there is less that READBLOCKSIZE space
206 * left in the buffer, it allocates a larger buffer and copies
207 * markNdx..curNdx from the old buffer into the new one. If the
208 * mark is not set, then it clears the buffer. It then tries to
209 * read READBLOCKSIZE from the underlying input stream.<p>
210 *
211 * Returns true iff not end-of-file, and at least one character
212 * was read from the file. Throws an IOException if no
213 * characters could be read from the stream.<p>
214 *
215 * Requires we are open.<p>
216 */
217
218 protected boolean refillBuf() throws IOException {
219 // Make sure need more characters in buffer:
220 Assert.notFalse( curNdx == endBufNdx );
221
222 // Slide buf down, keep from min( lastCharNdx, markNdx )
223 int minNdx = marked ? Math.min( lastCharNdx, markNdx ) : lastCharNdx;
224
225 if (buf.length - (curNdx - minNdx) < READBLOCKSIZE) {
226 // Allocate a new buffer
227 byte[] newBuf = new byte[ curNdx - minNdx + READBLOCKSIZE ];
228 System.arraycopy( buf, minNdx, newBuf, 0, curNdx - minNdx );
229 buf = newBuf;
230 } else {
231 System.arraycopy( buf, minNdx, buf, 0, curNdx-minNdx );
232 }
233 curNdx -= minNdx;
234 markNdx -= minNdx; //@ nowarn Unreadable;
235 lastCharNdx -= minNdx;
236 beforeBufLoc += minNdx;
237 endBufNdx = curNdx;
238
239 Assert.notFalse( endBufNdx+READBLOCKSIZE <= buf.length );
240
241 int got = 0;
242 do {
243 got = stream.read( buf, endBufNdx, READBLOCKSIZE );
244 } while (got == 0 );
245
246 if (got == -1) {
247 return false;
248 } else {
249 Assert.notFalse( curNdx == endBufNdx );
250 endBufNdx += got;
251 Assert.notFalse( endBufNdx <= buf.length );
252 Assert.notFalse( curNdx < endBufNdx );
253 return true;
254 }
255 }
256
257 // Misc
258
259 /**
260 * Returns the file underlying this correlated reader.
261 */
262
263 public GenericFile getFile() {
264 return file;
265 }
266 }