Agda.Utils.Pretty

Pretty printing functions.

Pretty class

class Pretty a where

While Show is for rendering data in Haskell syntax, Pretty is for displaying data to the world, i.e., the user and the environment.

Atomic data has no inner document structure, so just implement pretty as pretty a = text $ ... a ....

Minimal complete definition

Nothing

Methods

pretty :: a -> Doc

prettyPrec :: Int -> a -> Doc

Instances

Pretty Char

Pretty Int

Pretty Int32

Pretty Integer

Pretty String

Pretty Doc

Pretty CPUTime

Print CPU time in milli (10^-3) seconds.

Pretty Relevance

Pretty Induction

Pretty TopLevelModuleName

Pretty QName

Pretty NamePart

Pretty Name

Pretty GenPart

Pretty Notation

Pretty Fixity

Pretty Fixity'

Pretty Order

Pretty CallMatrix

Pretty ModuleName

Pretty QName

Pretty Name

Pretty Literal

Pretty Pragma

Pretty OpenShortHand

Pretty ModuleApplication

Pretty Declaration

Pretty ImportedName

Pretty UsingOrHiding

Pretty ImportDirective

Pretty WhereClause

Pretty RHS

Pretty LHSCore

Pretty LHS

Pretty ColoredTypedBinding

Pretty TypedBinding

Pretty BoundName

Pretty TypedBindings

Pretty LamBinding

Pretty Pattern

Pretty Expr

Pretty Tel

Pretty LevelAtom

Pretty PlusLevel

Pretty Level

Pretty Sort

Pretty Type

Pretty Elim

Pretty Term

Pretty CompiledClauses

Pretty CallInfo

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).

Pretty [Declaration]

Pretty [Pattern]

Pretty a => Pretty (Lisp a)

Pretty a => Pretty (Position' (Maybe a))

Pretty e => Pretty (Named_ e)

Pretty (ThingWithFixity Name)

Pretty cinfo => Pretty (CMSet cinfo)

Pretty cinfo => Pretty (CallMatrixAug cinfo)

Pretty cinfo => Pretty (CallGraph cinfo)

Displays the recursion behaviour corresponding to a call graph.

Pretty (OpApp Expr)

Pretty e => Pretty (Arg e)

Pretty a => Pretty (Arg a)

Pretty a => Pretty (Case a)

Pretty a => Pretty (WithArity a)

(Pretty a, Pretty b) => Pretty (a, b)

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

Pretty instances

Doc utilities

pwords :: String -> [Doc]

fwords :: String -> Doc

mparens :: Bool -> Doc -> Doc

align :: Int -> [(String, Doc)] -> Doc

align max rows lays out the elements of rows in two columns, with the second components aligned. The alignment column of the second components is at most max characters to the right of the left-most column.

Precondition: max > 0.

module Text.PrettyPrint