fmrisc.ProofNavigator.SWT

Class TextInputStream

java.lang.Object

java.io.InputStream

fmrisc.ProofNavigator.SWT.TextInputStream

All Implemented Interfaces:

java.io.Closeable, java.lang.AutoCloseable, java.util.EventListener, org.eclipse.swt.events.KeyListener, org.eclipse.swt.internal.SWTEventListener

public final class TextInputStream
extends java.io.InputStream
implements org.eclipse.swt.events.KeyListener

Mapping of a Text widget to an InputStream object.

Constructor Summary

Constructors

Constructor and Description
TextInputStream(org.eclipse.swt.widgets.Text input, java.io.PrintWriter echo, java.nio.charset.Charset charSet) Create an input stream from a Text widget.

Method Summary

Methods

Modifier and Type	Method and Description
void	append(java.lang.String text) Append text to buffer and notify waiting reader.
int	available() Get number of bytes available on stream.
void	close() close stream
void	keyPressed(org.eclipse.swt.events.KeyEvent e) Listener method that is invoked when input is entered in widget.
void	keyReleased(org.eclipse.swt.events.KeyEvent e) Listener method that is invoked when key is released in widget.
int	read() Read a character from this stream.
int	read(byte[] b, int offset, int length) Write into buffer b at position offset at most length bytes.

Methods inherited from class java.io.InputStream

mark, markSupported, read, reset, skip

Methods inherited from class java.lang.Object

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

Constructor Detail

TextInputStream

public TextInputStream(org.eclipse.swt.widgets.Text input,
               java.io.PrintWriter echo,
               java.nio.charset.Charset charSet)

Create an input stream from a Text widget.

Parameters:

input - the widget that provides the data for the input stream.

echo - writer to which the input is to be echoed (null, if no echo)

charSet - the character set to be used for encoding

Method Detail

keyReleased

public void keyReleased(org.eclipse.swt.events.KeyEvent e)

Listener method that is invoked when key is released in widget.

Specified by:

keyReleased in interface org.eclipse.swt.events.KeyListener

Parameters:

e - the event raised

keyPressed

public void keyPressed(org.eclipse.swt.events.KeyEvent e)

Listener method that is invoked when input is entered in widget.

Specified by:

keyPressed in interface org.eclipse.swt.events.KeyListener

Parameters:

e - the event raised

append

public void append(java.lang.String text)

Append text to buffer and notify waiting reader.

Parameters:

text - text to be appended to buffer.

available

public int available()

Get number of bytes available on stream.

Overrides:

available in class java.io.InputStream

Returns:

number of bytes available on stream

read

public int read(byte[] b,
       int offset,
       int length)

Write into buffer b at position offset at most length bytes.

Overrides:

read in class java.io.InputStream

Parameters:

b - the byte buffer to be filled (may be null)

offset - the distance from the start of the buffer where the filling shall start.

length - the maximum number of bytes to be written to the buffer.

Returns:

the actual number of bytes written.

read

public int read()

Read a character from this stream.

Specified by:

read in class java.io.InputStream

Returns:

the character

close

public void close()
           throws java.io.IOException

close stream

Specified by:

close in interface java.io.Closeable

Specified by:

close in interface java.lang.AutoCloseable

Overrides:

close in class java.io.InputStream

Throws:

java.io.IOException