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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Pretty

Contents

Description

Pretty printing functions.

Synopsis

Documentation

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

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

Pretty instances

Doc utilities

pwords :: 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.