Package net.sourceforge.czt.print.z

Provides classes for printing standard Z specifications in Unicode or in the LaTeX mark-up language.

See:
Description

Interface Summary

AbstractPrintVisitor.ZPrinter	A printer that can print Z symbols.
ZPrintVisitor.Utils

Class Summary

AbstractPrintVisitor	A Z visitor used for printing.
AstToPrintTreeVisitor	This visitor transforms an AST into a print tree, that is an AST prepared for printing.
ContextFreeScanner	The context-free lexer for Z specifications in unicode format.
DefsWord
LatexPrinterCommand
NewlineScanner	This scanner gets token from another scanner and provides them to the parser, but removes some of the NL tokens.
OldLatexPrinterCommand
PrecedenceParenAnnVisitor	This visitor visits an printable AST and adds necessary parentheses.
PrecedenceVisitor	Throws NullPointerException if no operator table is given but a term that needs a lookup in the operator table.
PrintUtils	Utilities for printing Z specifications given as an AST.
SectHeadScanner	This is a scanner that creates SECTHEAD tokens of type ZSect for section headers.
Sym	CUP generated class containing symbol constants.
ToSpiveyZVisitor	A translator to Spivey Z AST.
Unicode2Latex	CUP v0.11a beta 20060608 generated parser.
Unicode2OldLatex	CUP v0.11a beta 20060608 generated parser.
UnicodePrinter	Print Z specifications in Unicode.
UnicodePrinterCommand
UnicodeToLatex	Unicode to Latex transformation utilities for Standard Z.
WhereWord
XmlPrinterCommand
ZmlScanner	This Scanner uses the print visitor to tokenize a given Z term.
ZmlScanner.SymbolCollector	An implementation of AbstractPrintVisitor.ZPrinter.
ZPrintVisitor	A Z visitor used for printing.
ZPrintVisitor.UtilsImpl

Exception Summary

AstToPrintTreeVisitor.CannotPrintAstException

Package net.sourceforge.czt.print.z Description

Provides classes for printing standard Z specifications in Unicode or in the LaTeX mark-up language.

The Unicode2Latex parser together with the UnicodeScanner can be used to transform a Z specification written in unicode into a specification in LaTex without building an intermediate AST. The class UnicodeToLatex provides convenience methods and a command line tool for doing this.

An existing AST can be printed using the ZPrintVisitor together with the ZmlScanner. The ZPrintVisitor returns a list of Symbols which is tokenized by the ZmlScanner. The UnicodePrinter can be used to print the tokenized specification in unicode, whereas the Unicode2Latex parser can be used to print the tokenized specification in LaTex.

However, in most cases the AST must be preprocessed to get good, or even useful, results. The EqualPredVisitor transforms the default representation of equality to a representation via a relational operator that can be processed by the ZPrintVisitor.