de.uka.ilkd.pp
Class Layouter<Exc extends java.lang.Exception>

java.lang.Object
  de.uka.ilkd.pp.Layouter<Exc>

Type Parameters:

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

Direct Known Subclasses:

DataLayouter

public class Layouter<Exc extends java.lang.Exception>
extends java.lang.Object

Pretty-print information formatted using line breaks and indentation. For instance, this class can be used to print

 while (i > 0) {
   i--;
   j++;
 }
 

instead of

 while (i > 0) { i
 --; j++;}
 

if a maximum line width of 15 characters is chosen.

The formatted output is directed to a backend which might write it to an I/O stream, append it to the text of a GUI componenet or store it in a string. The Backend interface encapsulates the concept of backend. Apart from handling the output, the backend is also asked for the available line width and for the amount of space needed to print a string. This makes it possible to include e.g. HTML markup in the output which does not take up any space. There are two convenience implementations WriterBackend and StringBackend, which write the output to a Writer, resp. a String.

The layouter internally keeps track of a current indentation level. Think of nicely indented Java source code. Then the indentation level at any point is the number of blank columns to be inserted at the begining of the next line if you inserted a line break. To increase the indentation level of parts of the text, the input to the layouter is separated into blocks. The indentation level changes when a block is begun, and it is reset to its previous value when a block is ended. Of course, blocks maybe nested. In order to break text among several lines, the layouter needs to be told where line breaks are allowed. A break is a position in the text where there is either a line break (with appropriate indentation) or a number of spaces, if enough material fits in one line. In order to handle the indentation level properly, breaks should only occur inside blocks. There are in fact two kinds of blocks: consistent and inconsistent ones. In a consistent block, lines are broken either at all or at none of the breaks. In an inconsistent block, as much material as possible is put on one line before it is broken.

Consider the program above. It should be printed either as

 while (i > 0) { i--; j++; }
 

or, if there is not enough space on the line, as

 while (i > 0) {
   i--;
   j++;
 }
 

Given a Layouter object l, we could say:

 l.beginC(2).print("while (i>0) {").brk(1,0)
  .print("i--;").brk(1,0)
  .print("j++;").brk(1,-2)
  .print("}").end();
 

The call to beginC(int) starts a consistent block, advancing the indentation level by 2, relative to the current position in the line. The print(String) methods gives some actual text to be output. The call to brk(int,int) inserts a break. The first argument means that one space should be printed at this position if the line is not broken. The second argument is an offset to be added to the indentation level for the next line, if the line is broken. The effect of this parameter can be seen in the call brk(1,-2). The offset of -2 outdents the last line by 2 positions, which aligns the closing brace with the while.

If the lines in a block are broken, one sometimes wants to insert spaces up to the current indentation level at a certain position without allowing a line break there. This can be done using the ind(int,int) method. For instance, one wants to output either

   ...[Good and Bad and Ugly]...
 

or

   ...[    Good
       and Bad
       and Ugly]...
 

Note the four spaces required before Good. We do this by opening a block which sets the indentation level to the column where the G ends up and outdenting the lines with the and:

 l.print("...[").beginC(4).ind(0, 0).print("Good").brk(1, -4).print("and ")
                .print("Bad").brk(1, -4).print("and ").print("Ugly").end()
                .print("]...");
 

Again, the first argument to ind(int,int) is a number of spaces to print if the block we are in is printed on one line. The second argument is an offset to be added to the current indentation level to determine the column to which we should skip.

When all text has been sent to a Layouter and all blocks have been ended, the close() method should be closed. This sends all pending output to the backend and invokes the Backend.close() method, which usually closes I/O streams, etc.

The indentation level of a new block can be increased either relative to the current position on the line, or relative to the surrounding block's indentation level. Using the current position is useful e.g. to produce output like

 if x>=2 then x := x-2
         else x := x+2
 

where beginning a block in front of the then can set the indentation level to the current position in the line without knowing how much space the condition took up. Indenting by 3 relative to the surrounding block's indentation level would produce

 if x>=2 then x := x-2
    else x := x+2
 

no matter where in the first line the block was opened.

Some applications need to keep track of where certain parts of the input text end up in the output. For this purpose, the Layouter class provides the mark(Object) method.

The public methods of this class may be divided into two categories: A small number of primitive methods, as described above, and a host of convenience methods which simplify calling the primitive ones for often-used arguments. For instance, a call to beginC() is shorthand for beginC(ind), where ind is the default indentation selected when the Layouter was constructed.

Most of the methods can throw an UnbalancedBlocksException, which indicates that the sequence of method calls was illegal, i.e. more blocks were ended than begun, the Layouter is closed before all blocks are ended, a break occurs outside of any block, etc.

The backend might throw exceptions of the type indicated by the type parameter Exc. Such exceptions get passed through to the caller of the Layouter. Note that since text usually gets buffered before it is sent to the backend, exceptions thrown by calls to Layouter methods might not be caused directly by that method call but by an earlier one getting forwarded to the backend.

The algorithm used is essentially the classical one from Derek C. Oppen: Prettyprinting, TOPLAS volume 2 number 4, ACM, 1980, pp. 465-483, with some minor extensions. It has the property that if the input contains enough actual text, i.e. not just arbitrarily long sequences of calls to beginC, mark, etc., then pretty-printing uses constant space, and time linear in the size of the input. In fact, output will begin before the whole input has been given, so this class can be used to pretty-print a stream of data.

Author:

Martin Giese

See Also:

Backend

Nested Class Summary

static class	Layouter.BreakConsistency An enum type to distinguish consistent and inconsistent blocks.
static class	Layouter.IndentationBase An enum type to distinguish indentation relative to the current position or relative to the surrounding block's indentation level

Field Summary

static int	DEFAULT_INDENTATION = 2 : The default indentation for some of the convenience constructors
static int	DEFAULT_LINE_WIDTH = 80 : The line width for some of the convenience factories.

Constructor Summary

Layouter(Backend<Exc> back, int indentation)
Construts a newly allocated Layouter which will send output to the given Backend and has the given default indentation.

Method Summary

Layouter<Exc>	begin(boolean consistent) Deprecated. use begin(de.uka.ilkd.pp.Layouter.BreakConsistency, de.uka.ilkd.pp.Layouter.IndentationBase, int)
Layouter<Exc>	begin(boolean consistent, int indent) Deprecated. use begin(de.uka.ilkd.pp.Layouter.BreakConsistency, de.uka.ilkd.pp.Layouter.IndentationBase, int)
Layouter<Exc>	begin(Layouter.BreakConsistency cons, Layouter.IndentationBase indBase, int indent) Begin a block.
Layouter<Exc>	beginC() Begin a consistent block.
Layouter<Exc>	beginC(int indent) Begin a consistent block.
Layouter<Exc>	beginCInd() Begin a consistent block.
Layouter<Exc>	beginCInd(int indent) Begin a consistent block.
Layouter<Exc>	beginI() Begin an inconsistent block.
Layouter<Exc>	beginI(int indent) Begin an inconsistent block.
Layouter<Exc>	beginIInd() Begin an inconsistent block.
Layouter<Exc>	beginIInd(int indent) Begin an inconsistent block.
Layouter<Exc>	brk() Print a break with zero offset and width one.
Layouter<Exc>	brk(int width) Print a break with zero offset.
Layouter<Exc>	brk(int width, int offset) Print a break.
void	close() Close the Layouter.
Layouter<Exc>	end() Ends the innermost block.
Layouter<Exc>	flush() Output any information currently kept in buffers.
static Layouter<NoExceptions>	getStringLayouter(java.lang.StringBuilder sb) Factory method for a Layouter with a StringBackend.
static Layouter<NoExceptions>	getStringLayouter(java.lang.StringBuilder sb, int lineWidth) Factory method for a Layouter with a StringBackend.
static Layouter<NoExceptions>	getStringLayouter(java.lang.StringBuilder sb, int lineWidth, int indentation) Factory method for a Layouter with a StringBackend.
static Layouter<java.io.IOException>	getWriterLayouter(java.io.Writer writer) Factory method for a Layouter with a WriterBackend.
static Layouter<java.io.IOException>	getWriterLayouter(java.io.Writer writer, int lineWidth) Factory method for a Layouter with a WriterBackend.
static Layouter<java.io.IOException>	getWriterLayouter(java.io.Writer writer, int lineWidth, int indentation) Factory method for a Layouter with a WriterBackend.
Layouter<Exc>	ind() Indent with zero offset and zero width.
Layouter<Exc>	ind(int width, int offset) Indent relative to the indentation level if surrounding block is broken.
Layouter<Exc>	mark(java.lang.Object o) This leads to a call of the Backend.mark(Object) method of the backend, when the material preceding the call to mark has been printed to the backend, including any inserted line breaks and indentation.
Layouter<Exc>	nl() Print a break with zero offset and large width.
Layouter<Exc>	pre(java.lang.String s) Layout prefromated text.
Layouter<Exc>	print(java.lang.String s) Output text material.

Methods inherited from class java.lang.Object

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

Field Detail

DEFAULT_LINE_WIDTH

public static final int DEFAULT_LINE_WIDTH

= 80 : The line width for some of the convenience factories.

See Also:

Constant Field Values

DEFAULT_INDENTATION

public static final int DEFAULT_INDENTATION

= 2 : The default indentation for some of the convenience constructors

See Also:

Constant Field Values

Constructor Detail

Layouter

public Layouter(Backend<Exc> back,
                int indentation)

Construts a newly allocated Layouter which will send output to the given Backend and has the given default indentation.

Parameters:

back - the Backend

indentation - the default indentation

Method Detail

getWriterLayouter

public static Layouter<java.io.IOException> getWriterLayouter(java.io.Writer writer)

Factory method for a Layouter with a WriterBackend. The line width is taken to be DEFAULT_LINE_WIDTH, and the default indentation DEFAULT_INDENTATION.

Parameters:

writer - the Writer the Backend is going to use

getWriterLayouter

public static Layouter<java.io.IOException> getWriterLayouter(java.io.Writer writer,
                                                              int lineWidth)

Factory method for a Layouter with a WriterBackend. The default indentation is taken from DEFAULT_INDENTATION.

Parameters:

writer - the Writer the Backend is going to use

lineWidth - the maximum lineWidth the Backend is going to use

getWriterLayouter

public static Layouter<java.io.IOException> getWriterLayouter(java.io.Writer writer,
                                                              int lineWidth,
                                                              int indentation)

Factory method for a Layouter with a WriterBackend.

Parameters:

writer - the Writer the Backend is going to use

lineWidth - the maximum lineWidth the Backend is going to use

indentation - the default indentation

getStringLayouter

public static Layouter<NoExceptions> getStringLayouter(java.lang.StringBuilder sb)

Factory method for a Layouter with a StringBackend. The line width is taken to be DEFAULT_LINE_WIDTH, and the default indentation DEFAULT_INDENTATION.

Parameters:

sb - the StringBuilder the Backend is going to use

getStringLayouter

public static Layouter<NoExceptions> getStringLayouter(java.lang.StringBuilder sb,
                                                       int lineWidth)

Factory method for a Layouter with a StringBackend. The default indentation is taken from DEFAULT_INDENTATION.

Parameters:

sb - the StringBuilder the Backend is going to use

lineWidth - the maximum lineWidth the Backend is going to use

getStringLayouter

public static Layouter<NoExceptions> getStringLayouter(java.lang.StringBuilder sb,
                                                       int lineWidth,
                                                       int indentation)

Factory method for a Layouter with a StringBackend.

Parameters:

sb - the StringBuilder the Backend is going to use

lineWidth - the maximum lineWidth the Backend is going to use

indentation - the default indentation

print

public Layouter<Exc> print(java.lang.String s)
                                                throws Exc extends java.lang.Exception

Output text material. The string s should not contain newline characters. If you have a string with newline characters, and want to retain its formatting, consider using the pre(String s) method. The Layouter will not insert any line breaks in such a string.

Parameters:

s - the String to print.

Returns:

this

Throws:

Exc extends java.lang.Exception

begin

public Layouter<Exc> begin(Layouter.BreakConsistency cons,
                           Layouter.IndentationBase indBase,
                           int indent)

Begin a block. Parameter cons indicates whether this is a consistent block or an inconsistent one. In consistent blocks, breaks are either all broken or none is broken. The indentation level is increased by indent, either relative to the current position, or relative to the surrounding block's indentation level, depending on the parameter indBase.

Parameters:

cons - true for consistent block

indBase - increment relative to current pos, not indentation

indent - increment to indentation level

Returns:

this

end

public Layouter<Exc> end()
                                              throws Exc extends java.lang.Exception

Ends the innermost block.

Returns:

this

Throws:

Exc extends java.lang.Exception

brk

public Layouter<Exc> brk(int width,
                         int offset)
                                              throws Exc extends java.lang.Exception

Print a break. This will print width spaces if the line is not broken at this point. If it is broken, indentation is added to the current indentation level, plus the value of offset.

Parameters:

width - space to insert if not broken

offset - offset relative to current indentation level

Returns:

this

Throws:

Exc extends java.lang.Exception

ind

public Layouter<Exc> ind(int width,
                         int offset)
                                              throws Exc extends java.lang.Exception

Indent relative to the indentation level if surrounding block is broken. If the surrounding block fits on one line, insert width spaces. Otherwise, indent to the current indentation level, plus offset, unless that position has already been exceeded on the current line. If that is the case, nothing is printed. No line break is possible at this point.

Parameters:

width - space to insert if not broken

offset - offset relative to current indentation level

Returns:

this

Throws:

Exc extends java.lang.Exception

mark

public Layouter<Exc> mark(java.lang.Object o)
                                               throws Exc extends java.lang.Exception

This leads to a call of the Backend.mark(Object) method of the backend, when the material preceding the call to mark has been printed to the backend, including any inserted line breaks and indentation. The Object argument to mark is passed through unchanged to the backend and may be used by the application to pass information about the purpose of the mark.

Parameters:

o - an object to be passed through to the backend.

Returns:

this

Throws:

Exc extends java.lang.Exception

flush

public Layouter<Exc> flush()
                                                throws Exc extends java.lang.Exception

Output any information currently kept in buffers. This is essentially passed on to the backend. Note that material in blocks begun but not ended cannot be forced to the output by this method. Finish all blocks and call flush or close() then.

Returns:

this

Throws:

Exc extends java.lang.Exception

close

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

Close the Layouter. No more methods should be called after this. All blocks begun must have been ended by this point. Any pending material is written to the backend, before the Backend.close() method of the backend is called, which closes any open I/O streams, etc.

Throws:

Exc extends java.lang.Exception

begin

public Layouter<Exc> begin(boolean consistent,
                           int indent)

Deprecated. use begin(de.uka.ilkd.pp.Layouter.BreakConsistency, de.uka.ilkd.pp.Layouter.IndentationBase, int)

Begin a block. If consistent is set, breaks are either all broken or all not broken. The indentation level is increased by indent, relative to the current position.

Parameters:

consistent - true for consistent block

indent - increment to indentation level

Returns:

this

beginI

public Layouter<Exc> beginI()

Begin an inconsistent block. Increment the indentation level by this layouter's default indentation, relative to the current position.

Returns:

this

beginC

public Layouter<Exc> beginC()

Begin a consistent block. Increment the indentation level by this layouter's default indentation, relative to the current position.

Returns:

this

beginI

public Layouter<Exc> beginI(int indent)

Begin an inconsistent block. Add indent to the indentation level, relative to the current position.

Parameters:

indent - the indentation for this block

Returns:

this

beginC

public Layouter<Exc> beginC(int indent)

Begin a consistent block. Add indent to the indentation level, relative to the current position.

Parameters:

indent - the indentation for this block

Returns:

this

begin

public Layouter<Exc> begin(boolean consistent)

Deprecated. use begin(de.uka.ilkd.pp.Layouter.BreakConsistency, de.uka.ilkd.pp.Layouter.IndentationBase, int)

Begin a block with default indentation. Add this Layouter's default indentation to the indentation level, relative to the current position.

Parameters:

consistent - true for consistent block

Returns:

this

beginIInd

public Layouter<Exc> beginIInd()

Begin an inconsistent block. Increment the indentation level by this layouter's default indentation, relative to the surrounding block's indentation level.

Returns:

this

beginCInd

public Layouter<Exc> beginCInd()

Begin a consistent block. Increment the indentation level by this layouter's default indentation, relative to the surrounding block's indentation level.

Returns:

this

beginIInd

public Layouter<Exc> beginIInd(int indent)

Begin an inconsistent block. Increment the indentation level by indent, relative to the surrounding block's indentation level.

Parameters:

indent - the indentation for this block

Returns:

this

beginCInd

public Layouter<Exc> beginCInd(int indent)

Begin a consistent block. Increment the indentation level by indent, relative to the surrounding block's indentation level.

Parameters:

indent - the indentation for this block

Returns:

this

brk

public Layouter<Exc> brk(int width)
                                              throws Exc extends java.lang.Exception

Print a break with zero offset.

Parameters:

width - space to insert if not broken

Returns:

this

Throws:

Exc extends java.lang.Exception

brk

public Layouter<Exc> brk()
                                              throws Exc extends java.lang.Exception

Print a break with zero offset and width one.

Returns:

this

Throws:

Exc extends java.lang.Exception

nl

public Layouter<Exc> nl()
                                             throws Exc extends java.lang.Exception

Print a break with zero offset and large width. As the large number of spaces will never fit into one line, this amounts to a forced line break.

Returns:

this

Throws:

Exc extends java.lang.Exception

ind

public Layouter<Exc> ind()
                                              throws Exc extends java.lang.Exception

Indent with zero offset and zero width. Just indents to the current indentation level if the block is broken, and prints nothing otherwise.

Returns:

this

Throws:

Exc extends java.lang.Exception

pre

public Layouter<Exc> pre(java.lang.String s)
                                              throws Exc extends java.lang.Exception

Layout prefromated text. This amounts to a (consistent) block with indentation 0, where each line of s (separated by \n) gets printed as a string and newlines become forced breaks.

Parameters:

s - the pre-formatted string

Returns:

this

Throws:

Exc extends java.lang.Exception