Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Agda.Utils.Pretty
Contents
Description
Pretty printing functions.
Synopsis
- class Pretty a where
- pretty :: a -> Doc
- prettyPrec :: Int -> a -> Doc
- prettyList :: [a] -> Doc
- prettyShow :: Pretty a => a -> String
- pwords :: String -> [Doc]
- fwords :: String -> Doc
- prettyList_ :: Pretty a => [a] -> Doc
- mparens :: Bool -> Doc -> Doc
- align :: Int -> [(String, Doc)] -> Doc
- multiLineText :: String -> Doc
- (<?>) :: Doc -> Doc -> Doc
- pshow :: Show a => a -> Doc
- fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc -> a
- renderStyle :: Style -> Doc -> String
- render :: Doc -> String
- fsep :: [Doc] -> Doc
- fcat :: [Doc] -> Doc
- cat :: [Doc] -> Doc
- sep :: [Doc] -> Doc
- (<+>) :: Doc -> Doc -> Doc
- (<>) :: Doc -> Doc -> Doc
- ($+$) :: Doc -> Doc -> Doc
- ($$) :: Doc -> Doc -> Doc
- punctuate :: Doc -> [Doc] -> [Doc]
- hang :: Doc -> Int -> Doc -> Doc
- nest :: Int -> Doc -> Doc
- vcat :: [Doc] -> Doc
- hsep :: [Doc] -> Doc
- hcat :: [Doc] -> Doc
- braces :: Doc -> Doc
- brackets :: Doc -> Doc
- parens :: Doc -> Doc
- doubleQuotes :: Doc -> Doc
- quotes :: Doc -> Doc
- rational :: Rational -> Doc
- double :: Double -> Doc
- float :: Float -> Doc
- integer :: Integer -> Doc
- int :: Int -> Doc
- rbrace :: Doc
- lbrace :: Doc
- rbrack :: Doc
- lbrack :: Doc
- rparen :: Doc
- lparen :: Doc
- equals :: Doc
- space :: Doc
- colon :: Doc
- comma :: Doc
- semi :: Doc
- isEmpty :: Doc -> Bool
- zeroWidthText :: String -> Doc
- sizedText :: Int -> String -> Doc
- ptext :: String -> Doc
- text :: String -> Doc
- char :: Char -> Doc
- data Doc
- style :: Style
- pattern Chr :: !Char -> TextDetails
- pattern PStr :: String -> TextDetails
- data Style = Style {
- mode :: Mode
- lineLength :: Int
- ribbonsPerLine :: Float
- data Mode
Documentation
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
Instances
prettyList_ :: Pretty a => [a] -> Doc Source #
Comma separated list, without the brackets.
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
.
multiLineText :: String -> Doc Source #
Handles strings with newlines properly (preserving indentation)
Arguments
:: Mode | Rendering mode. |
-> Int | Line length. |
-> Float | Ribbons per line. |
-> (TextDetails -> a -> a) | What to do with text. |
-> a | What to do at the end. |
-> Doc | The document. |
-> a | Result. |
The general rendering interface. Please refer to the Style
and Mode
types for a description of rendering mode, line length and ribbons.
($$) :: Doc -> Doc -> Doc infixl 5 Source #
Above, except that if the last line of the first argument stops at least one position before the first line of the second begins, these two lines are overlapped. For example:
text "hi" $$ nest 5 (text "there")
lays out as
hi there
rather than
hi there
punctuate :: Doc -> [Doc] -> [Doc] Source #
punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]
nest :: Int -> Doc -> Doc Source #
Nest (or indent) a document by a given number of positions
(which may also be negative). nest
satisfies the laws:
nest
0 x = xnest
k (nest
k' x) =nest
(k+k') xnest
k (x<>
y) =nest
k x<>
nest
k ynest
k (x$$
y) =nest
k x$$
nest
k ynest
kempty
=empty
x
, if<>
nest
k y = x<>
yx
non-empty
The side condition on the last law is needed because
empty
is a left identity for <>
.
zeroWidthText :: String -> Doc Source #
Some text, but without any width. Use for non-printing text such as a HTML or Latex tags
sizedText :: Int -> String -> Doc Source #
Some text with any width. (text s = sizedText (length s) s
)
The abstract type of documents. A Doc represents a set of layouts. A Doc with no occurrences of Union or NoDoc represents just one layout.
Instances
Eq Doc | |
Data Doc Source # | |
Defined in Agda.Utils.Pretty Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc Source # toConstr :: Doc -> Constr Source # dataTypeOf :: Doc -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) Source # gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source # | |
Show Doc | |
IsString Doc | |
Defined in Text.PrettyPrint.HughesPJ Methods fromString :: String -> Doc Source # | |
Generic Doc | |
Semigroup Doc | |
Monoid Doc | |
NFData Doc | |
Defined in Text.PrettyPrint.HughesPJ | |
Null Doc Source # | |
Pretty Doc Source # | |
Underscore Doc Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Doc Source # | |
Null (TCM Doc) Source # | |
type Rep Doc | |
Defined in Text.PrettyPrint.HughesPJ |
pattern Chr :: !Char -> TextDetails Source #
A single Char fragment
pattern PStr :: String -> TextDetails Source #
Used to represent a Fast String fragment but now deprecated and identical to the Str constructor.
A rendering style. Allows us to specify constraints to choose among the many different rendering options.
Constructors
Style | |
Fields
|
Instances
Eq Style | |
Show Style | |
Generic Style | |
type Rep Style | |
Defined in Text.PrettyPrint.Annotated.HughesPJ type Rep Style = D1 (MetaData "Style" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" False) (C1 (MetaCons "Style" PrefixI True) (S1 (MetaSel (Just "mode") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Mode) :*: (S1 (MetaSel (Just "lineLength") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :*: S1 (MetaSel (Just "ribbonsPerLine") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Float)))) |
Rendering mode.
Constructors
PageMode | Normal rendering ( |
ZigZagMode | With zig-zag cuts. |
LeftMode | No indentation, infinitely long lines ( |
OneLineMode | All on one line, |
Instances
Eq Mode | |
Show Mode | |
Generic Mode | |
type Rep Mode | |
Defined in Text.PrettyPrint.Annotated.HughesPJ type Rep Mode = D1 (MetaData "Mode" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" False) ((C1 (MetaCons "PageMode" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "ZigZagMode" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "LeftMode" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "OneLineMode" PrefixI False) (U1 :: Type -> Type))) |
Orphan instances
Data Doc Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc Source # toConstr :: Doc -> Constr Source # dataTypeOf :: Doc -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) Source # gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc Source # |