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    }