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 }