public class CountingBufferedReader
extends java.io.BufferedReader
Constructor and Description |
---|
CountingBufferedReader(java.io.InputStream in) |
CountingBufferedReader(java.io.InputStream in,
int size,
int step) |
CountingBufferedReader(java.io.InputStream in,
ProgressMonitor monitor,
int step) |
CountingBufferedReader(java.io.InputStream in,
ProgressMonitor monitor,
int step,
int alreadyRead) |
Modifier and Type | Method and Description |
---|---|
int |
getNumberOfParsedChars() |
int |
read() |
int |
read(char[] cbuf,
int off,
int len) |
java.lang.String |
readLine() |
long |
skip(long n) |
public CountingBufferedReader(java.io.InputStream in)
public CountingBufferedReader(java.io.InputStream in, ProgressMonitor monitor, int step)
public CountingBufferedReader(java.io.InputStream in, ProgressMonitor monitor, int step, int alreadyRead)
public CountingBufferedReader(java.io.InputStream in, int size, int step)
public int read() throws java.io.IOException
read
in class java.io.BufferedReader
java.io.IOException
public int read(char[] cbuf, int off, int len) throws java.io.IOException
read
in class java.io.BufferedReader
java.io.IOException
public java.lang.String readLine() throws java.io.IOException
readLine
in class java.io.BufferedReader
java.io.IOException
public long skip(long n) throws java.io.IOException
skip
in class java.io.BufferedReader
java.io.IOException
public int getNumberOfParsedChars()
Copyright © 2003-2019 The KeY-Project.