escjava.prover
Class TeeOutputStream

java.lang.Object
  java.io.OutputStream
      java.io.FilterOutputStream
          escjava.prover.TeeOutputStream

public class TeeOutputStream

extends java.io.FilterOutputStream

This class is a FilterOutputStream class that forwards its given output to two given OutputStreams.

Version:

11 Aug 2000

Author:

Rustan Leino

Field Summary

protected java.io.OutputStream

out2 The other underlying output stream to be filtered (the first being out in the superclass).

Fields inherited from class java.io.FilterOutputStream

out

Constructor Summary

TeeOutputStream(java.io.OutputStream out0, java.io.OutputStream out1)
Creates an output stream filter built on top of two specified underlying output streams.

Method Summary

void	close() Closes this output stream and releases any system resources associated with the stream.
void	flush() Flushes this output stream and forces any buffered output bytes to be written out to the stream.
void	write(byte[] b) Writes b.length bytes to this output stream.
void	write(byte[] b, int off, int len) Writes len bytes from the specified byte array starting at offset off to this output stream.
void	write(int b) Writes the specified byte to this output stream.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

out2

protected java.io.OutputStream out2

The other underlying output stream to be filtered (the first being out in the superclass).

Constructor Detail

TeeOutputStream

public TeeOutputStream(java.io.OutputStream out0,
                       java.io.OutputStream out1)

Creates an output stream filter built on top of two specified underlying output streams.

Parameters:

out0 - the first of the underlying output streams; will be assigned to this.out; should not be null

out1 - the second of the underlying output streams; will be assigned to this.out2; should not be null

Method Detail

write

public void write(int b)
           throws java.io.IOException

Writes the specified byte to this output stream.

The write method of TeeOutputStream calls the write method of its two underlying output streams, that is, it performs out.write(b) and then out2.write(b).

Implements the abstract write method of OutputStream.

Parameters:

b - the byte.

Throws:

java.io.IOException - if an I/O error occurs.

write

public void write(byte[] b)
           throws java.io.IOException

Writes b.length bytes to this output stream.

The write method of TeeOutputStream calls the write method of its two underlying output streams, that is, it performs out.write(b) and then out2.write(b).

Parameters:

b - the data to be written.

Throws:

java.io.IOException - if an I/O error occurs.

See Also:

FilterOutputStream.write(byte[], int, int)

write

public void write(byte[] b,
                  int off,
                  int len)
           throws java.io.IOException

Writes len bytes from the specified byte array starting at offset off to this output stream.

The write method of TeeOutputStream calls the write method of its two underlying output streams, that is, it performs out.write(b) and then out2.write(b).

Parameters:

b - the data.

off - the start offset in the data.

len - the number of bytes to write.

Throws:

java.io.IOException - if an I/O error occurs.

See Also:

FilterOutputStream.write(int)

flush

public void flush()
           throws java.io.IOException

Flushes this output stream and forces any buffered output bytes to be written out to the stream.

The flush method of FilterOutputStream calls the flush method of its two underlying output streams.

Throws:

java.io.IOException - if an I/O error occurs.

See Also:

FilterOutputStream.flush()

close

public void close()
           throws java.io.IOException

Closes this output stream and releases any system resources associated with the stream.

The close method of FilterOutputStream calls its flush method, and then calls the close method of its two underlying output streams.

Throws:

java.io.IOException - if an I/O error occurs.

See Also:

FilterOutputStream.flush(), FilterOutputStream.close()