    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    }