fmrisc.ProofNavigator.SWT

Class TextOutputStream

java.lang.Object

java.io.OutputStream

fmrisc.ProofNavigator.SWT.TextOutputStream

All Implemented Interfaces:

java.io.Closeable, java.io.Flushable, java.lang.AutoCloseable

public final class TextOutputStream
extends java.io.OutputStream

Mapping of an OutputStream object to a Text widget.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
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