Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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 `OutputStream`s.

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()`

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage