| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Pretty
Contents
Description
Pretty printing functions.
Synopsis
- class Pretty a where
- 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 ....
Instances
prettyShow :: Pretty a => a -> String #
Use instead of show when printing to world.
prettyList_ :: Pretty a => [a] -> Doc #
Comma separated list, without the brackets.
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.
multiLineText :: String -> Doc #
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.
renderStyle :: Style -> Doc -> String #
Render the Doc to a String using the given Style.
($$) :: Doc -> Doc -> Doc infixl 5 #
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
therepunctuate :: Doc -> [Doc] -> [Doc] #
punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]
Nest (or indent) a document by a given number of positions
(which may also be negative). nest satisfies the laws:
nest0 x = xnestk (nestk' x) =nest(k+k') xnestk (x<>y) =nestk x<>nestk ynestk (x$$y) =nestk x$$nestk ynestkempty=emptyx, if<>nestk y = x<>yxnon-empty
The side condition on the last law is needed because
empty is a left identity for <>.
zeroWidthText :: String -> Doc #
Some text, but without any width. Use for non-printing text such as a HTML or Latex tags
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 # | |
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc # dataTypeOf :: Doc -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) # gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r # gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc # | |
| Show Doc | |
| IsString Doc | |
Defined in Text.PrettyPrint.HughesPJ Methods fromString :: String -> Doc # | |
| Generic Doc | |
| Semigroup Doc | |
| Monoid Doc | |
| NFData Doc | |
Defined in Text.PrettyPrint.HughesPJ | |
| Null Doc # | |
| Pretty Doc # | |
Defined in Agda.Utils.Pretty | |
| Underscore Doc # | |
Defined in Agda.Syntax.Common | |
| EmbPrj Doc # | |
| Null (TCM Doc) # | |
| type Rep Doc | |
Defined in Text.PrettyPrint.HughesPJ | |
pattern Chr :: !Char -> TextDetails #
A single Char fragment
pattern PStr :: String -> TextDetails #
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 :: * -> *) :+: C1 (MetaCons "ZigZagMode" PrefixI False) (U1 :: * -> *)) :+: (C1 (MetaCons "LeftMode" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "OneLineMode" PrefixI False) (U1 :: * -> *))) | |
Orphan instances
| Data Doc # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc # dataTypeOf :: Doc -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc) # gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r # gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc # | |