001    /* $Id: PPOutputStream.java,v 1.5 2006/08/05 10:59:08 chalin Exp $ */
002    /* Copyright 2000, 2001, Compaq Computer Corporation */
003    
004    package escjava.prover;
005    
006    import java.io.OutputStream;
007    import java.io.FilterOutputStream;
008    import java.io.IOException;
009    
010    
011    /**
012      * This class is a FilterOutputStream class designed for LISP-like
013      * input; it pretty prints the output by inserting spaces and newlines
014      * into the stream.
015      *
016      * @author  David Cok
017      */
018    
019    public class PPOutputStream extends FilterOutputStream {
020    
021        private int parenDepth = 0;
022        private boolean inComment = false;
023        private boolean recentNL = false;
024    
025        static final int lp = '(';
026        static final int rp = ')';
027    
028        /**
029         * Creates an output stream filter built on top of an
030         * underlying output streams.
031         *
032         * @param   out   the underlying output stream
033         */
034        public PPOutputStream(/*@ non_null */ OutputStream out) {
035            super(out);
036        }
037    
038        /**
039         * Writes the specified <code>byte</code> to this output stream. 
040         * <p>
041         * Implements the abstract <tt>write</tt> method of <tt>OutputStream</tt>. 
042         *
043         * @param      b   the <code>byte</code>.
044         * @exception  IOException  if an I/O error occurs.
045         */
046        //@ also private normal_behavior
047        //@   assignable inComment, parenDepth, recentNL;
048        public void write(int b) throws IOException {
049            if (inComment) {
050                    super.write(b);
051                    if (b == '\n' || b == '\r') {
052                            inComment = false;
053                    } else {
054                            return;
055                    }
056            }
057            if (b == ';') {
058                    inComment = true;
059                    super.write(b);
060                    return;
061            }
062            if (b == lp) {
063                if (!recentNL) {
064                    super.write('\n'); //FIXME - multiplatform ???
065                    int n = 2*parenDepth;
066                    while (--n >= 0) super.write(' ');
067                }
068                ++parenDepth;
069            }
070    
071            if (b == rp) {
072                super.write(b);
073                super.write('\n'); //FIXME - multiplatform ???
074                --parenDepth;
075                int n = 2*parenDepth;
076                while (--n >= 0) super.write(' ');
077                recentNL = true;
078            } else if (b == ' ' || b == '\t') {
079                if (!recentNL) super.write(b);
080            } else if (b == '\n' || b == '\r') {
081                if (!recentNL) {
082                    super.write(b);
083                    int n = 2*parenDepth;
084                    while (--n >= 0) super.write(' ');
085                    if (parenDepth > 0) recentNL = true;
086                }
087            } else {
088                super.write(b);
089                recentNL = false;
090            }
091    
092        }
093    
094    }