    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    import java.io.OutputStream;
    006    import java.io.FilterOutputStream;
    007    import java.io.IOException;
    008
    009
    010    /**
    011      * This class is a FilterOutputStream class designed for LISP-like
    012      * input; it pretty prints the output by inserting spaces and newlines
    013      * into the stream.
    014      *
    015      * @author  David Cok
    016      */
    017
    018    public class PPOutputStream extends FilterOutputStream {
    019
    020        int parenDepth = 0;
    021        boolean inComment = false;
    022        static final int lp = '(';
    023        static final int rp = ')';
    024
    025        /**
    026         * Creates an output stream filter built on top of an
    027         * underlying output streams.
    028         *
    029         * @param   out   the underlying output stream
    030         */
    031        public PPOutputStream(/*@ non_null */ OutputStream out) {
    032            super(out);
    033        }
    034
    035        /**
    036         * Writes the specified <code>byte</code> to this output stream.
    037         * <p>
    038         * Implements the abstract <tt>write</tt> method of <tt>OutputStream</tt>.
    039         *
    040         * @param      b   the <code>byte</code>.
    041         * @exception  IOException  if an I/O error occurs.
    042         */
    043        public void write(int b) throws IOException {
    044            if (inComment) {
    045                    super.write(b);
    046                    if (b == '\n' || b == '\r') {
    047                            inComment = false;
    048                    } else {
    049                            return;
    050                    }
    051            }
    052            if (b == ';') {
    053                    inComment = true;
    054                    super.write(b);
    055                    return;
    056            }
    057            if (b == lp) {
    058                if (!recentNL) {
    059                    super.write('\n'); //FIXME - multiplatform ???
    060                    int n = 2*parenDepth;
    061                    while (--n >= 0) super.write(' ');
    062                }
    063                ++parenDepth;
    064            }
    065
    066            if (b == rp) {
    067                super.write(b);
    068                super.write('\n'); //FIXME - multiplatform ???
    069                --parenDepth;
    070                int n = 2*parenDepth;
    071                while (--n >= 0) super.write(' ');
    072                recentNL = true;
    073            } else if (b == ' ' || b == '\t') {
    074                if (!recentNL) super.write(b);
    075            } else if (b == '\n' || b == '\r') {
    076                if (!recentNL) {
    077                    super.write(b);
    078                    int n = 2*parenDepth;
    079                    while (--n >= 0) super.write(' ');
    080                    if (parenDepth > 0) recentNL = true;
    081                }
    082            } else {
    083                super.write(b);
    084                recentNL = false;
    085            }
    086
    087        }
    088
    089        boolean recentNL = false;
    090        /**
    091         * Writes <code>b.length</code> bytes to this output stream.
    092         * <p>
    093         *
    094         * @param      b   the data to be written.
    095         * @exception  IOException  if an I/O error occurs.
    096         * @see        java.io.FilterOutputStream#write(byte[], int, int)
    097         */
    098        public void write(byte b[]) throws IOException {
    099            write(b,0,b.length);
    100        }
    101
    102        /**
    103         * Writes <code>len</code> bytes from the specified
    104         * <code>byte</code> array starting at offset <code>off</code> to
    105         * this output stream.
    106         * <p>
    107         *
    108         * @param      b     the data.
    109         * @param      off   the start offset in the data.
    110         * @param      len   the number of bytes to write.
    111         * @exception  IOException  if an I/O error occurs.
    112         * @see        java.io.FilterOutputStream#write(int)
    113         */
    114    /*
    115        public void write(byte b[], int off, int len) throws IOException {
    116            int e = off+len;
    117            int n = len;
    118            int i = off;
    119            while (i<e) {
    120                byte bb = b[i];
    121                if (bb == lp) {
    122                    super.write(b,off,i-off);
    123                    off = i;
    124                    super.write('\n'); //FIXME - multiplatform ???
    125                    int nn = 2*parenDepth;
    126                    while (--nn >= 0) super.write(' ');
    127                    ++parenDepth;
    128                    ++i;
    129
    130                } else if (bb == rp) {
    131                    ++i;
    132                    super.write(b,off,i-off);
    133                    off = i;
    134                    --parenDepth;
    135                    super.write('\n'); //FIXME - multiplatform ???
    136                    int nn = 2*parenDepth;
    137                    while (--nn >= 0) super.write(' ');
    138
    139                } else {
    140                    ++i;
    141                }
    142            }
    143            super.write(b, off, e-off);
    144        }
    145    */
    146        /**
    147         * Flushes this output stream and forces any buffered output bytes
    148         * to be written out to the stream.
    149         * <p>
    150         *
    151         * @exception  IOException  if an I/O error occurs.
    152         * @see        java.io.FilterOutputStream#flush
    153         */
    154        public void flush() throws IOException {
    155            super.flush();
    156        }
    157
    158        /**
    159         * Closes this output stream and releases any system resources
    160         * associated with the stream.
    161         * <p>
    162         *
    163         * @exception  IOException  if an I/O error occurs.
    164         * @see        java.io.FilterOutputStream#flush()
    165         * @see        java.io.FilterOutputStream#close
    166         */
    167        public void close() throws IOException {
    168            try {
    169              flush();
    170            } catch (IOException ignored) {
    171            }
    172            super.close();
    173        }
    174    }