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    }