|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object java.io.InputStream fmrisc.ProofNavigator.SWT.TextInputStream
public final class TextInputStream
Mapping of a Text widget to an InputStream object.
Constructor Summary | |
---|---|
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 | |
---|---|
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 |
---|
public TextInputStream(org.eclipse.swt.widgets.Text input, java.io.PrintWriter echo, java.nio.charset.Charset charSet)
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 encodingMethod Detail |
---|
public void keyReleased(org.eclipse.swt.events.KeyEvent e)
keyReleased
in interface org.eclipse.swt.events.KeyListener
e
- the event raisedpublic void keyPressed(org.eclipse.swt.events.KeyEvent e)
keyPressed
in interface org.eclipse.swt.events.KeyListener
e
- the event raisedpublic void append(java.lang.String text)
text
- text to be appended to buffer.public int available()
available
in class java.io.InputStream
public int read(byte[] b, int offset, int length)
read
in class java.io.InputStream
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.
public int read()
read
in class java.io.InputStream
public void close() throws java.io.IOException
close
in interface java.io.Closeable
close
in class java.io.InputStream
java.io.IOException
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |