Agda-2.4.2.4: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Pretty

Contents

Description

Pretty printing functions.

Synopsis

Pretty class

class Pretty a where Source

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 Source

prettyPrec :: Int -> a -> Doc Source

Instances

Pretty Bool Source 
Pretty Char Source 
Pretty Int Source 
Pretty Int32 Source 
Pretty Integer Source 
Pretty String Source 
Pretty Doc Source 
Pretty AbsolutePath Source 
Pretty CPUTime Source

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

Pretty Phase Source 
Pretty Order Source 
Pretty CallMatrix Source 
Pretty TopLevelModuleName Source 
Pretty QName Source 
Pretty NamePart Source 
Pretty Name Source 
Pretty AmbiguousQName Source 
Pretty ModuleName Source 
Pretty QName Source 
Pretty Name Source 
Pretty Literal Source 
Pretty Tel Source 
Pretty DeclarationException Source 
Pretty ParseError Source 
Pretty Substitution Source 
Pretty MetaId Source 
Pretty LevelAtom Source 
Pretty PlusLevel Source 
Pretty Level Source 
Pretty Sort Source 
Pretty Type Source 
Pretty Elim Source 
Pretty Term Source 
Pretty CompiledClauses Source 
Pretty CallInfo Source 
Pretty Call Source 
Pretty NamedMeta Source 
Pretty Comparison Source 
Pretty Interface Source 
Pretty ProblemId Source 
Pretty CallPath Source

Only show intermediate nodes. (Drop last CallInfo).

Pretty a => Pretty (Lisp a) Source 
(Ord a, Pretty a) => Pretty (Benchmark a) Source

Print benchmark as two-column table with totals.

Pretty cinfo => Pretty (CMSet cinfo) Source 
Pretty cinfo => Pretty (CallMatrixAug cinfo) Source 
Pretty cinfo => Pretty (CallGraph cinfo) Source

Displays the recursion behaviour corresponding to a call graph.

(Pretty a, HasRange a) => Pretty (PrintRange a) Source 
Pretty a => Pretty (Range' (Maybe a)) Source 
Pretty a => Pretty (Interval' (Maybe a)) Source 
Pretty a => Pretty (Position' (Maybe a)) Source 
Pretty a => Pretty (QNamed a) Source 
Pretty a => Pretty (Arg a) Source 
Pretty a => Pretty (Case a) Source 
Pretty a => Pretty (WithArity a) Source 
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source 
(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source 

prettyShow :: Pretty a => a -> String Source

Use instead of show when printing to world.

Pretty instances

Doc utilities

pwords :: String -> [Doc] Source

fwords :: String -> Doc Source

mparens :: Bool -> Doc -> Doc Source

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

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