fmrisc.ProofNavigator.Communication

Class PrettyPrinter

java.lang.Object

fmrisc.ProofNavigator.Communication.PrettyPrinter

public final class PrettyPrinter
extends java.lang.Object

Printing abstract syntax trees with appropriate line breaks.

Field Summary

Fields

Modifier and Type	Field and Description
static int	WIDTH The pretty printer depends on the current printing mode (LINE or BLOCK) and the current indentation level LEVEL.

Constructor Summary

Constructors

Constructor and Description
PrettyPrinter(int width, java.io.PrintWriter out) Create pretty printer to print abstract syntax trees.
PrettyPrinter(java.io.PrintWriter out) Create pretty printer for default width WIDTH.

Method Summary

Modifier and Type	Method and Description
void	changeLevel(boolean increase) Change indentation level.
void	newLine() Start new (non-overflow)line and indent it appropriately.
void	print(Declaration decl) Pretty-print declaration.
void	print(Expression exp) Pretty-print expression.
void	print(java.lang.String text) Print text.
void	print(Type type) Pretty-print type.
void	space() Insert a space (or a newline at the end of the line).

Methods inherited from class java.lang.Object

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

Field Detail

WIDTH

public static final int WIDTH

The pretty printer depends on the current printing mode (LINE or BLOCK) and the current indentation level LEVEL. Printing a tree starts in BLOCK mode, when a subtree is encountered that demands switching to LINE mode, the whole subtree is printed in LINE mode (no switching back to BLOCK mode within the subtree). When printed in LINE mode, a syntax tree fills the current line as much as possible; if a line break has to be inserted, the remainder of the tree is printed at increased level LEVEL+1 (not further increased). token token token token token ... LEVEL token token token token token token LEVEL+1 token token token token token token LEVEL+1 The only trees that make use of the BLOCK mode are the ones listed below. If such a tree does not fit into the current line, parts of it are printed at indentation level LEVEL+1 (which may be further increased within the parts). IDENT:"TYPE"= LEVEL TYPE LEVEL+1 IDENT:TYPE = LEVEL EXPRESSION; LEVEL+1 IDENT:("FORMULA"|"AXIOM") = LEVEL FORMULA LEVEL+1 QUANTIFIER(VARIABLES): LEVEL EXPRESSION LEVEL+1 FORMULA LEVEL+1 BINARY-CONNECTIVE LEVEL FORMULA LEVEL+1 BINARY-CONNECTIVE LEVEL FORMULA LEVEL+1 IF FORMULA THEN LEVEL EXPRESSION LEVEL+1 ELSIF FORMULA THEN LEVEL EXPRESSION LEVEL+1 ELSE LEVEL EXPRESSION LEVEL+1 ENDIF LEVEL LET LEVEL DECLARATION, LEVEL+1 DECLARATION, LEVEL+1 DECLARATION LEVEL+1 IN LEVEL EXPRESSION LEVEL+1 The indentation level is not increased beyond MAXLEVEL; if this bound is reached, the corresponding subtree is printed in LINE mode. Likewise, if the number of character positions in a line drops below MINFREE, the remainder of the tree is printed in LINE mode.

See Also:

Constant Field Values

Constructor Detail

PrettyPrinter

public PrettyPrinter(int width,
                     java.io.PrintWriter out)

Create pretty printer to print abstract syntax trees.

Parameters:

width - the line width (suggestion, not a hard bound).

out - the stream to print on.

PrettyPrinter

public PrettyPrinter(java.io.PrintWriter out)

Create pretty printer for default width WIDTH.

Parameters:

out - the stream to print on.

Method Detail

print

public void print(Declaration decl)

Pretty-print declaration.

Parameters:

decl - a declaration.

print

public void print(Expression exp)

Pretty-print expression.

Parameters:

exp - an expression.

print

public void print(Type type)

Pretty-print type.

Parameters:

type - a type

print

public void print(java.lang.String text)

Print text.

Parameters:

text - the text to be printed.

changeLevel

public void changeLevel(boolean increase)

Change indentation level.

Parameters:

increase - true if level is increased (decreased otherwise)

newLine

public void newLine()

Start new (non-overflow)line and indent it appropriately.

space

public void space()

Insert a space (or a newline at the end of the line).