de.uka.ilkd.pp
Interface Backend<Exc extends java.lang.Exception>

Type Parameters:

Exc - The type of exceptions that might be thrown by this backend.

All Known Implementing Classes:

StringBackend, WriterBackend

public interface Backend<Exc extends java.lang.Exception>

The backend for a Layouter. An object satisfying this interface can act as a receiver for the layed out text produced by a Layouter. A Backend must also provide the maximum line width available through the lineWidth() method. Finally, it is responsible for calculating (with measure(String) the amount of space it actually needs to print a given string. For instance, if strings printed through a Layouter are actually known to be in HTML, measure(String) can return the size of the text, not including markup.

This interface has a type parameter Exc which denotes the type of exceptions that might be thrown when output is sent to a backend. For instance, a backend like WriterBackend, which ultimately writes output to a Writer might produce IOExceptions which should not be handled by the Backend, but passed through to the program calling the Layouter. So it implements the interface Backend<java.io.IOException>. There is a dummy exception class NoExceptions that may be used as parameter if no checked exceptions are thrown by a Backend.

There is currently no provision to handle proportional fonts, and there might never be.

Author:

Martin Giese

See Also:

Layouter

Method Summary

void	close() Closes 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.

Method Detail

print

void print(java.lang.String s)
           throws Exc extends java.lang.Exception

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

Throws:

Exc extends java.lang.Exception

newLine

void newLine()
             throws Exc extends java.lang.Exception

Start a new line.

Throws:

Exc extends java.lang.Exception

close

void close()
           throws Exc extends java.lang.Exception

Closes this backend

Throws:

Exc extends java.lang.Exception

flush

void flush()
           throws Exc extends java.lang.Exception

Flushes any buffered output

Throws:

Exc extends java.lang.Exception

mark

void mark(java.lang.Object o)
          throws Exc extends java.lang.Exception

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

Throws:

Exc extends java.lang.Exception

lineWidth

int lineWidth()

Returns the available space per line

measure

int measure(java.lang.String s)

Returns the space required to print the String s