org.extex.main.tex
Class TeXInputReader

java.lang.Object
  java.io.Reader
      org.extex.main.tex.TeXInputReader

All Implemented Interfaces:

java.io.Closeable, java.lang.Readable

public class TeXInputReader
extends java.io.Reader

This Reader gets the characters from System.in but presents a prompt before each line of input.

Version:

$Revision:4445 $

Author:

Gerd Neugebauer

Field Summary

Fields inherited from class java.io.Reader

lock

Constructor Summary

TeXInputReader(java.util.logging.Logger logger, java.lang.String charset, Interpreter interpreter)
Creates a new object.

Method Summary

void	close()
boolean	markSupported()
int	read()
int	read(char[] buffer)
int	read(char[] buffer, int startIndex, int len)
boolean	ready()
void	reset()
long	skip(long n)

Methods inherited from class java.io.Reader

mark, read

Methods inherited from class java.lang.Object

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

Constructor Detail

TeXInputReader

public TeXInputReader(java.util.logging.Logger logger,
                      java.lang.String charset,
                      Interpreter interpreter)
               throws java.io.UnsupportedEncodingException

Creates a new object.

Parameters:

logger - the logger to write to

charset - the character set to use

interpreter - the interpreter

Throws:

java.io.UnsupportedEncodingException - in case that the encoding is not known

Method Detail

close

public void close()
           throws java.io.IOException

Specified by:

close in interface java.io.Closeable

Specified by:

close in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.close()

markSupported

public boolean markSupported()

Overrides:

markSupported in class java.io.Reader

See Also:

Reader.markSupported()

read

public int read()
         throws java.io.IOException

Overrides:

read in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.read()

read

public int read(char[] buffer)
         throws java.io.IOException

Overrides:

read in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.read(char[])

read

public int read(char[] buffer,
                int startIndex,
                int len)
         throws java.io.IOException

Specified by:

read in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.read(char[], int, int)

ready

public boolean ready()
              throws java.io.IOException

Overrides:

ready in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.ready()

reset

public void reset()
           throws java.io.IOException

Overrides:

reset in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.reset()

skip

public long skip(long n)
          throws java.io.IOException

Overrides:

skip in class java.io.Reader

Throws:

java.io.IOException

See Also:

Reader.skip(long)