| java.lang.Object de.uka.ilkd.key.util.pp.Printer
Printer | class Printer (Code) | | The intermediate layer of the pretty printing library. Using the
block size information provided by the
Layouter class, this
decides where to insert line breaks. It tries to break as few
blocks as possible.
|
Method Summary | |
void | close() Close the output stream. | void | closeBlock() | void | flush() Flush the output stream. | void | indent(int width, int offset) | int | lineWidth() Return the line width of this Printer. | void | mark(Object o) | void | openBlock(boolean consistent, int indent, int followingLength) | void | print(String s) | void | printBreak(int width, int offset, int followingLength) write a break. | int | space() Return the amount of space currently left on this line. |
Printer | Printer(Backend back)(Code) | | Create a printer. It will write its output to writer .
Lines have a maximum width of lineWidth .
|
closeBlock | void closeBlock()(Code) | | end a block
|
lineWidth | int lineWidth()(Code) | | Return the line width of this Printer.
|
openBlock | void openBlock(boolean consistent, int indent, int followingLength)(Code) | | begin a block
|
printBreak | void printBreak(int width, int offset, int followingLength) throws IOException(Code) | | write a break. followingLength should be the
space needed by the material up to the next corresponding
closeBlock() or printBreak(), and is used to decide whether the
current line is continues, or a new (indented) line is begun.
|
space | int space()(Code) | | Return the amount of space currently left on this line.
|
|
|