org.overturetool.vdmj.lex
Class LatexStreamReader

java.lang.Object
  java.io.Reader
      java.io.InputStreamReader
          org.overturetool.vdmj.lex.LatexStreamReader

All Implemented Interfaces:

java.io.Closeable, java.lang.Readable

public class LatexStreamReader
extends java.io.InputStreamReader

A class to read LaTeX encoded VDM files.

Field Summary

Fields inherited from class java.io.Reader

lock

Constructor Summary

LatexStreamReader(java.io.InputStream in, java.lang.String charsetName)

Method Summary

int	read(char[] array)

Methods inherited from class java.io.InputStreamReader

close, getEncoding, read, read, ready

Methods inherited from class java.io.Reader

mark, markSupported, read, reset, skip

Methods inherited from class java.lang.Object

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

Constructor Detail

LatexStreamReader

public LatexStreamReader(java.io.InputStream in,
                         java.lang.String charsetName)
                  throws java.io.UnsupportedEncodingException

Throws:

java.io.UnsupportedEncodingException

Method Detail

read

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

Overrides:

read in class java.io.Reader

Throws:

java.io.IOException