de.uka.ilkd.pp
Class WriterBackend

java.lang.Object
  de.uka.ilkd.pp.WriterBackend

All Implemented Interfaces:

Backend<java.io.IOException>

public class WriterBackend
extends java.lang.Object
implements Backend<java.io.IOException>

A Backend which writes all output to a java.io.Writer. The mark(Object o) method does nothing in this implementation. There is a method count() which returns the number of characters written by this so far.

Field Summary

protected int	count
protected int	lineWidth
protected java.io.Writer	out

Constructor Summary

WriterBackend(java.io.Writer w, int lineWidth)

Method Summary

void	close() Closes this backend
int	count() Returns the number of characters written through this backend.
void	flush() Flushes any buffered output
int	lineWidth() Returns the available space per line
void	mark(java.lang.Object o) Gets called to record a mark() call in the input.
int	measure(java.lang.String s) Returns the space required to print the String s
void	newLine() Start a new line.
void	print(java.lang.String s) Append a String s to the output.

Methods inherited from class java.lang.Object

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

Field Detail

out

protected java.io.Writer out

lineWidth

protected int lineWidth

count

protected int count

Constructor Detail

WriterBackend

public WriterBackend(java.io.Writer w,
                     int lineWidth)

Method Detail

print

public void print(java.lang.String s)
           throws java.io.IOException

Append a String s to the output. s contains no newlines.

Specified by:

print in interface Backend<java.io.IOException>

Throws:

java.io.IOException

newLine

public void newLine()
             throws java.io.IOException

Start a new line.

Specified by:

newLine in interface Backend<java.io.IOException>

Throws:

java.io.IOException

close

public void close()
           throws java.io.IOException

Closes this backend

Specified by:

close in interface Backend<java.io.IOException>

Throws:

java.io.IOException

flush

public void flush()
           throws java.io.IOException

Flushes any buffered output

Specified by:

flush in interface Backend<java.io.IOException>

Throws:

java.io.IOException

mark

public void mark(java.lang.Object o)

Gets called to record a mark() call in the input.

Specified by:

mark in interface Backend<java.io.IOException>

count

public int count()

Returns the number of characters written through this backend.

lineWidth

public int lineWidth()

Returns the available space per line

Specified by:

lineWidth in interface Backend<java.io.IOException>

measure

public int measure(java.lang.String s)

Returns the space required to print the String s

Specified by:

measure in interface Backend<java.io.IOException>