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

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

Type Parameters:

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

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

An extension of Layouter to print arbitrary Java data. There is a print(Object) method that prints objects according to their type. In particular, there are special layouts for (nested) collections, maps, and arrays. Classes implementing the interface PrettyPrintable provide their own method for printing themselves to a DataLayouter.

Like most methods of Layouter, the methods of this class return this, so calls can be sequenced as in l.beginC().print(...).brk(...).

The intended main use of this class is to produce more readable debugging output than what System.err.println() would give, or for data output that should be human-readable. It produces standard representations of data, like Object.toString(). Application-specific types will usually wish to define their own pretty printing, using the methods of Layouter.

Author:

Martin Giese

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.pp.Layouter

Layouter.BreakConsistency, Layouter.IndentationBase

Field Summary

Fields inherited from class de.uka.ilkd.pp.Layouter

DEFAULT_INDENTATION, DEFAULT_LINE_WIDTH

Constructor Summary

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

Method Summary

DataLayouter<Exc>	begin(boolean consistent) Deprecated. use begin(de.uka.ilkd.pp.Layouter.BreakConsistency, de.uka.ilkd.pp.Layouter.IndentationBase, int)
DataLayouter<Exc>	begin(boolean consistent, int indent) Deprecated. use begin(de.uka.ilkd.pp.Layouter.BreakConsistency, de.uka.ilkd.pp.Layouter.IndentationBase, int)
DataLayouter<Exc>	begin(Layouter.BreakConsistency consistent, Layouter.IndentationBase fromPos, int indent) Begin a block.
DataLayouter<Exc>	beginC() Begin a consistent block.
DataLayouter<Exc>	beginC(int indent) Begin a consistent block.
DataLayouter<Exc>	beginCInd() Begin a consistent block.
DataLayouter<Exc>	beginCInd(int indent) Begin a consistent block.
DataLayouter<Exc>	beginI() Begin an inconsistent block.
DataLayouter<Exc>	beginI(int indent) Begin an inconsistent block.
DataLayouter<Exc>	beginIInd() Begin an inconsistent block.
DataLayouter<Exc>	beginIInd(int indent) Begin an inconsistent block.
DataLayouter<Exc>	brk() Print a break with zero offset and width one.
DataLayouter<Exc>	brk(int width) Print a break with zero offset.
DataLayouter<Exc>	brk(int width, int offset) Print a break.
DataLayouter<Exc>	end() Ends the innermost block.
DataLayouter<Exc>	flush() Output any information currently kept in buffers.
static DataLayouter<java.io.IOException>	getWriterDataLayouter(java.io.Writer writer) Factory method for a DataLayouter with a WriterBackend.
static DataLayouter<java.io.IOException>	getWriterDataLayouter(java.io.Writer writer, int lineWidth) Factory method for a DataLayouter with a WriterBackend.
static DataLayouter<java.io.IOException>	getWriterDataLayouter(java.io.Writer writer, int lineWidth, int indentation) Factory method for a DataLayouter with a WriterBackend.
DataLayouter<Exc>	ind() Indent with zero offset and zero width.
DataLayouter<Exc>	ind(int width, int offset) Indent relative to the indentation level if surrounding block is broken.
DataLayouter<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.
DataLayouter<Exc>	nl() Print a break with zero offset and large width.
DataLayouter<Exc>	pre(java.lang.String s) Layout prefromated text.
DataLayouter<Exc>	print(java.util.Collection<?> c) Print a collection.
DataLayouter<Exc>	print(java.util.Map<?,?> m) Print a map.
DataLayouter<Exc>	print(java.lang.Object o) Print o to this DataLayouter.
DataLayouter<Exc>	print(java.lang.String s) Output text material.
DataLayouter<Exc>	printArray(java.lang.Object o) Print an array of reference or primitive elements.
DataLayouter<Exc>	printEntry(java.util.Map.Entry<?,?> e) Print a map entry.

Methods inherited from class de.uka.ilkd.pp.Layouter

close, getStringLayouter, getStringLayouter, getStringLayouter, getWriterLayouter, getWriterLayouter, getWriterLayouter

Methods inherited from class java.lang.Object

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

Constructor Detail

DataLayouter

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

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

Parameters:

back - the Backend

indentation - the default indentation

Method Detail

getWriterDataLayouter

public static DataLayouter<java.io.IOException> getWriterDataLayouter(java.io.Writer writer)

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

Parameters:

writer - the Writer the Backend is going to use

getWriterDataLayouter

public static DataLayouter<java.io.IOException> getWriterDataLayouter(java.io.Writer writer,
                                                                      int lineWidth)

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

Parameters:

writer - the Writer the Backend is going to use

lineWidth - the maximum lineWidth the Backend is going to use

getWriterDataLayouter

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

Factory method for a DataLayouter 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

print

public DataLayouter<Exc> print(java.lang.Object o)
                                                    throws Exc extends java.lang.Exception

Print o to this DataLayouter. If o is an instance of PrettyPrintable, it is printed using its prettyPrint method. Otherwise, if o a is a collection, and array, or a map, it is printed as descibed in the methods print(Collection), printArray(Object), and print(Map), respectively. If everything else fails, o.toString() is used.

Parameters:

o - the object to be pretty printed

Throws:

Exc extends java.lang.Exception

print

public DataLayouter<Exc> print(java.util.Collection<?> c)
                                                    throws Exc extends java.lang.Exception

Print a collection. This is printed as

 [xxx, yyy, zzz]
 

if it fits on one line, and as

 [xxx,
  yyy,
  zzz]
 

otherwise.

Parameters:

c - A collection

Throws:

Exc extends java.lang.Exception

printArray

public DataLayouter<Exc> printArray(java.lang.Object o)
                                                         throws Exc extends java.lang.Exception

Print an array of reference or primitive elements. The produced layout is the same as for collections.

Parameters:

o - an object, has to be an array!

Throws:

Exc extends java.lang.Exception

print

public DataLayouter<Exc> print(java.util.Map<?,?> m)
                                                    throws Exc extends java.lang.Exception

Print a map. This is printed as

 {k1=v1, k2=v2, k3=v3]
 

if it fits on one line, and as

 {key1=val1,
  key2=val2,
  key3=val3]
 

otherwise. If values don't fit on one line, the key-value pairs will also be spread over two lines, as indicated for printEntry(java.util.Map.Entry).

Throws:

Exc extends java.lang.Exception

printEntry

public DataLayouter<Exc> printEntry(java.util.Map.Entry<?,?> e)
                                                         throws Exc extends java.lang.Exception

Print a map entry. This is printed as

 key=val
 

if it fits on one line, and as

 key=
   val
 

otherwise. This is mainly to prevent key from adding too much indentation.

Throws:

Exc extends java.lang.Exception

begin

public DataLayouter<Exc> begin(Layouter.BreakConsistency consistent,
                               Layouter.IndentationBase fromPos,
                               int indent)

Description copied from class: Layouter

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.

Overrides:

begin in class Layouter<Exc extends java.lang.Exception>

Parameters:

consistent - true for consistent block

fromPos - increment relative to current pos, not indentation

indent - increment to indentation level

Returns:

this

begin

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

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

Description copied from class: Layouter

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.

Overrides:

begin in class Layouter<Exc extends java.lang.Exception>

Parameters:

consistent - true for consistent block

indent - increment to indentation level

Returns:

this

begin

public DataLayouter<Exc> begin(boolean consistent)

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

Description copied from class: Layouter

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

Overrides:

begin in class Layouter<Exc extends java.lang.Exception>

Parameters:

consistent - true for consistent block

Returns:

this

beginC

public DataLayouter<Exc> beginC()

Description copied from class: Layouter

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

Overrides:

beginC in class Layouter<Exc extends java.lang.Exception>

Returns:

this

beginC

public DataLayouter<Exc> beginC(int indent)

Description copied from class: Layouter

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

Overrides:

beginC in class Layouter<Exc extends java.lang.Exception>

Parameters:

indent - the indentation for this block

Returns:

this

beginI

public DataLayouter<Exc> beginI()

Description copied from class: Layouter

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

Overrides:

beginI in class Layouter<Exc extends java.lang.Exception>

Returns:

this

beginI

public DataLayouter<Exc> beginI(int indent)

Description copied from class: Layouter

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

Overrides:

beginI in class Layouter<Exc extends java.lang.Exception>

Parameters:

indent - the indentation for this block

Returns:

this

beginCInd

public DataLayouter<Exc> beginCInd()

Description copied from class: Layouter

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

Overrides:

beginCInd in class Layouter<Exc extends java.lang.Exception>

Returns:

this

beginCInd

public DataLayouter<Exc> beginCInd(int indent)

Description copied from class: Layouter

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

Overrides:

beginCInd in class Layouter<Exc extends java.lang.Exception>

Parameters:

indent - the indentation for this block

Returns:

this

beginIInd

public DataLayouter<Exc> beginIInd()

Description copied from class: Layouter

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

Overrides:

beginIInd in class Layouter<Exc extends java.lang.Exception>

Returns:

this

beginIInd

public DataLayouter<Exc> beginIInd(int indent)

Description copied from class: Layouter

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

Overrides:

beginIInd in class Layouter<Exc extends java.lang.Exception>

Parameters:

indent - the indentation for this block

Returns:

this

brk

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

Description copied from class: Layouter

Print a break with zero offset and width one.

Overrides:

brk in class Layouter<Exc extends java.lang.Exception>

Returns:

this

Throws:

Exc extends java.lang.Exception

brk

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

Description copied from class: Layouter

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.

Overrides:

brk in class Layouter<Exc extends java.lang.Exception>

Parameters:

width - space to insert if not broken

offset - offset relative to current indentation level

Returns:

this

Throws:

Exc extends java.lang.Exception

brk

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

Description copied from class: Layouter

Print a break with zero offset.

Overrides:

brk in class Layouter<Exc extends java.lang.Exception>

Parameters:

width - space to insert if not broken

Returns:

this

Throws:

Exc extends java.lang.Exception

end

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

Description copied from class: Layouter

Ends the innermost block.

Overrides:

end in class Layouter<Exc extends java.lang.Exception>

Returns:

this

Throws:

Exc extends java.lang.Exception

flush

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

Description copied from class: Layouter

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 Layouter.close() then.

Overrides:

flush in class Layouter<Exc extends java.lang.Exception>

Returns:

this

Throws:

Exc extends java.lang.Exception

ind

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

Description copied from class: Layouter

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

Overrides:

ind in class Layouter<Exc extends java.lang.Exception>

Returns:

this

Throws:

Exc extends java.lang.Exception

ind

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

Description copied from class: Layouter

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.

Overrides:

ind in class Layouter<Exc extends java.lang.Exception>

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 DataLayouter<Exc> mark(java.lang.Object o)
                                                   throws Exc extends java.lang.Exception

Description copied from class: Layouter

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.

Overrides:

mark in class Layouter<Exc extends java.lang.Exception>

Parameters:

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

Returns:

this

Throws:

Exc extends java.lang.Exception

nl

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

Description copied from class: Layouter

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.

Overrides:

nl in class Layouter<Exc extends java.lang.Exception>

Returns:

this

Throws:

Exc extends java.lang.Exception

pre

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

Description copied from class: Layouter

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.

Overrides:

pre in class Layouter<Exc extends java.lang.Exception>

Parameters:

s - the pre-formatted string

Returns:

this

Throws:

Exc extends java.lang.Exception

print

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

Description copied from class: Layouter

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 Layouter.pre(String s) method. The Layouter will not insert any line breaks in such a string.

Overrides:

print in class Layouter<Exc extends java.lang.Exception>

Parameters:

s - the String to print.

Returns:

this

Throws:

Exc extends java.lang.Exception