fmrisc.ProofNavigator.SWT
Class TextOutputStream

java.lang.Object
  java.io.OutputStream
      fmrisc.ProofNavigator.SWT.TextOutputStream

All Implemented Interfaces:

java.io.Closeable, java.io.Flushable

public final class TextOutputStream
extends java.io.OutputStream

Mapping of an OutputStream object to a Text widget.

Constructor Summary

TextOutputStream(org.eclipse.swt.widgets.Text output, java.nio.charset.Charset charSet)
Create an output stream from a Text widget.

Method Summary

void	write(byte[] b) Write a byte array to the output stream.
void	write(byte[] b, int offset, int length) Write a section of an byte array to the output stream.
void	write(int b) Write a byte to the output stream.

Methods inherited from class java.io.OutputStream

close, flush

Methods inherited from class java.lang.Object

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

Constructor Detail

TextOutputStream

public TextOutputStream(org.eclipse.swt.widgets.Text output,
                        java.nio.charset.Charset charSet)

Create an output stream from a Text widget.

Parameters:

output - the widget that displays the output written to the stream.

charSet - the character set to be used for encoding

Method Detail

write

public void write(byte[] b,
                  int offset,
                  int length)

Write a section of an byte array to the output stream.

Overrides:

write in class java.io.OutputStream

Parameters:

b - the byte array.

offset - the array index where the section starts.

length - the length of the section.

write

public void write(byte[] b)

Write a byte array to the output stream.

Overrides:

write in class java.io.OutputStream

Parameters:

b - the byte array written

write

public void write(int b)

Write a byte to the output stream.

Specified by:

write in class java.io.OutputStream

Parameters:

b - the byte written