		Search-engine friendly clone of the ACL2 documentation.

Atj-implementation

Atj-java-pretty-printer

A pretty-printer for the abstract syntax of Java, for ATJ's implementation.

This pretty-printer produces text in the form of msgp and msg-listp values. The latter generally consist of lines of text; that is always the case at the top level, i.e. a Java compilation unit is turned into a list of lines. Some pretty-printing functions produce msgp values that other pretty-printing functions incorporate into larger text. In the pretty-printing functions, we consistently use the result names part for msgp values that are part of lines, parts for msg-listp values that are lists of parts of lines, line for msgp values that are individual lines, and lines for msg-listp values that are multiple lines.

A separate function writes the lines for a Java compilation unit to an output channel, which is associated to a file. The newline characters are added to this function; they do not appear in the msgp and msg-listp values.

Subtopics

Jexpr-rank: Ranks of expressions.
Print-jexprs: Pretty-printing of expressions.
Print-jchar: Pretty-print a character.
Print-jstatems+jblocks: Pretty-print a statement or block.
Print-jclasses+jcmembers: Pretty-print a class declaration or class member declaration.
Jbinop-expected-ranks: Expression ranks of the operands of a binary operator.
Jexpr->rank: Rank of an abstract syntactic expression.
Jexpr-rank-<=: Order over expression ranks.
Print-jexpr: Pretty-print an expression.
Print-optional-integer-type-suffix: Pretty-print an optional integer type suffix.
Print-octdig/uscore-list: Pretty-print a list of octal digits and underscores.
Print-oct-integer-literal: Pretty-print an octal integer literal.
Print-jcunit: Pretty-print a compilation unit.
Print-hexdig/uscore-list: Pretty-print a list of hexadecimal digits and underscores.
Print-hex-integer-literal: Pretty-print a hexadecimal integer literal.
Print-decdig/uscore-list: Pretty-print a list of decimal digits and underscores.
Print-dec-integer-literal: Pretty-print a decimal integer literal.
Print-bindig/uscore-list: Pretty-print a list of binary digits and underscores.
Print-bin-integer-literal: Pretty-print a binary integer literal.
Print-integer-literal: Pretty-print an integer literal.
Print-octdig/uscore: Pretty-print an octal digit or underscore.
Print-jmethod: Pretty-print a method declaration.
Print-jfield: Pretty-print a field declaration.
Print-hexdig/uscore: Pretty-print a hexadecimal digit or underscore.
Print-decdig/uscore: Pretty-print a decimal digit or underscore.
Print-bindig/uscore: Pretty-print a binary digit or underscore.
Print-jclass-list: Pretty-print a sequence of class declarations.
Print-jlocvar: Pretty-print a local variable declaration.
Print-jliteral: Pretty-print a literal.
Print-jcinitializer: Pretty-print a class initializer.
Print-jline: Pretty-print a (non-blank) line of code.
Print-jimports: Pretty-print a sequence of import declarations.
Print-jchars: Lift print-jchar to lists.
Print-comma-sep: Turn zero or more parts into a single part containing the initial parts, comma-separated.
Print-jimport: Pretty-print an import declaration.
Print-jbinop: Pretty-print a binary operator.
Print-primitive-type: Pretty-print a primitive type.
Print-jparam-list: Pretty-print a formal parameter list.
Print-jlines-to-channel: Write pretty-printed lines to an output channel.
Jexpr-rank-index
Atj-indent: Spaces from the left margin for the specified level of indentation.
Print-to-jfile: Write pretty-printed lines to a file.
Print-jparam: Pretty-print a formal parameter.
Print-jaccess: Pretty-print an access modifier.
Print-oct-digit: Pretty-print an octal digit.
Print-junop: Pretty-print a unary operator.
Print-jtype: Pretty-print a type.
Print-jresult: Pretty-print a method result.
Print-hex-digit: Pretty-print a hexadecimal digit.
Print-dec-digit: Pretty-print a decimal digit.
Print-bin-digit: Pretty-print a binary digit.
Print-jline-blank: Pretty-print a blank line of code.