Idris.Docstrings

Documentation

data Docstring a

Representation of Idris's inline documentation. The type paramter represents the type of terms that are associated with code blocks.

Constructors

DocString Options (Blocks a)

Instances

Functor Docstring

Defined in Idris.Docstrings

Methods

fmap :: (a -> b) -> Docstring a -> Docstring b

(<$) :: a -> Docstring b -> Docstring a

Foldable Docstring

Defined in Idris.Docstrings

Methods

fold :: Monoid m => Docstring m -> m

foldMap :: Monoid m => (a -> m) -> Docstring a -> m

foldr :: (a -> b -> b) -> b -> Docstring a -> b

foldr' :: (a -> b -> b) -> b -> Docstring a -> b

foldl :: (b -> a -> b) -> b -> Docstring a -> b

foldl' :: (b -> a -> b) -> b -> Docstring a -> b

foldr1 :: (a -> a -> a) -> Docstring a -> a

foldl1 :: (a -> a -> a) -> Docstring a -> a

toList :: Docstring a -> [a]

null :: Docstring a -> Bool

length :: Docstring a -> Int

elem :: Eq a => a -> Docstring a -> Bool

maximum :: Ord a => Docstring a -> a

minimum :: Ord a => Docstring a -> a

sum :: Num a => Docstring a -> a

product :: Num a => Docstring a -> a

Traversable Docstring

Defined in Idris.Docstrings

Methods

traverse :: Applicative f => (a -> f b) -> Docstring a -> f (Docstring b)

sequenceA :: Applicative f => Docstring (f a) -> f (Docstring a)

mapM :: Monad m => (a -> m b) -> Docstring a -> m (Docstring b)

sequence :: Monad m => Docstring (m a) -> m (Docstring a)

Show a => Show (Docstring a)

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> Docstring a -> ShowS

show :: Docstring a -> String

showList :: [Docstring a] -> ShowS

Generic (Docstring a)

Defined in Idris.Docstrings

Associated Types

type Rep (Docstring a) :: Type -> Type

Methods

from :: Docstring a -> Rep (Docstring a) x

to :: Rep (Docstring a) x -> Docstring a

Binary a => Binary (Docstring a)

Defined in Idris.IBC

Methods

put :: Docstring a -> Put

get :: Get (Docstring a)

putList :: [Docstring a] -> Put

NFData a => NFData (Docstring a)

Defined in Idris.DeepSeq

Methods

rnf :: Docstring a -> ()

type Rep (Docstring a)

Defined in Idris.Docstrings

type Rep (Docstring a)

data Block a

Block-level elements.

Constructors

Para (Inlines a)

Header Int (Inlines a)

Blockquote (Blocks a)

List Bool ListType [Blocks a]

CodeBlock CodeAttr Text a

HtmlBlock Text

HRule

Instances

Functor Block

Defined in Idris.Docstrings

Methods

fmap :: (a -> b) -> Block a -> Block b

(<$) :: a -> Block b -> Block a

Foldable Block

Defined in Idris.Docstrings

Methods

fold :: Monoid m => Block m -> m

foldMap :: Monoid m => (a -> m) -> Block a -> m

foldr :: (a -> b -> b) -> b -> Block a -> b

foldr' :: (a -> b -> b) -> b -> Block a -> b

foldl :: (b -> a -> b) -> b -> Block a -> b

foldl' :: (b -> a -> b) -> b -> Block a -> b

foldr1 :: (a -> a -> a) -> Block a -> a

foldl1 :: (a -> a -> a) -> Block a -> a

toList :: Block a -> [a]

null :: Block a -> Bool

length :: Block a -> Int

elem :: Eq a => a -> Block a -> Bool

maximum :: Ord a => Block a -> a

minimum :: Ord a => Block a -> a

sum :: Num a => Block a -> a

product :: Num a => Block a -> a

Traversable Block

Defined in Idris.Docstrings

Methods

traverse :: Applicative f => (a -> f b) -> Block a -> f (Block b)

sequenceA :: Applicative f => Block (f a) -> f (Block a)

mapM :: Monad m => (a -> m b) -> Block a -> m (Block b)

sequence :: Monad m => Block (m a) -> m (Block a)

Show a => Show (Block a)

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> Block a -> ShowS

show :: Block a -> String

showList :: [Block a] -> ShowS

Generic (Block a)

Defined in Idris.Docstrings

Associated Types

type Rep (Block a) :: Type -> Type

Methods

from :: Block a -> Rep (Block a) x

to :: Rep (Block a) x -> Block a

Binary a => Binary (Block a)

Defined in Idris.IBC

Methods

put :: Block a -> Put

get :: Get (Block a)

putList :: [Block a] -> Put

NFData a => NFData (Block a)

Defined in Idris.DeepSeq

Methods

rnf :: Block a -> ()

type Rep (Block a)

Defined in Idris.Docstrings

type Rep (Block a)

data Inline a

Constructors

Str Text

Space

SoftBreak

LineBreak

Emph (Inlines a)

Strong (Inlines a)

Code Text a

Link (Inlines a) Text Text

Image (Inlines a) Text Text

Entity Text

RawHtml Text

Instances

Functor Inline

Defined in Idris.Docstrings

Methods

fmap :: (a -> b) -> Inline a -> Inline b

(<$) :: a -> Inline b -> Inline a

Foldable Inline

Defined in Idris.Docstrings

Methods

fold :: Monoid m => Inline m -> m

foldMap :: Monoid m => (a -> m) -> Inline a -> m

foldr :: (a -> b -> b) -> b -> Inline a -> b

foldr' :: (a -> b -> b) -> b -> Inline a -> b

foldl :: (b -> a -> b) -> b -> Inline a -> b

foldl' :: (b -> a -> b) -> b -> Inline a -> b

foldr1 :: (a -> a -> a) -> Inline a -> a

foldl1 :: (a -> a -> a) -> Inline a -> a

toList :: Inline a -> [a]

null :: Inline a -> Bool

length :: Inline a -> Int

elem :: Eq a => a -> Inline a -> Bool

maximum :: Ord a => Inline a -> a

minimum :: Ord a => Inline a -> a

sum :: Num a => Inline a -> a

product :: Num a => Inline a -> a

Traversable Inline

Defined in Idris.Docstrings

Methods

traverse :: Applicative f => (a -> f b) -> Inline a -> f (Inline b)

sequenceA :: Applicative f => Inline (f a) -> f (Inline a)

mapM :: Monad m => (a -> m b) -> Inline a -> m (Inline b)

sequence :: Monad m => Inline (m a) -> m (Inline a)

Show a => Show (Inline a)

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> Inline a -> ShowS

show :: Inline a -> String

showList :: [Inline a] -> ShowS

Generic (Inline a)

Defined in Idris.Docstrings

Associated Types

type Rep (Inline a) :: Type -> Type

Methods

from :: Inline a -> Rep (Inline a) x

to :: Rep (Inline a) x -> Inline a

Binary a => Binary (Inline a)

Defined in Idris.IBC

Methods

put :: Inline a -> Put

get :: Get (Inline a)

putList :: [Inline a] -> Put

NFData a => NFData (Inline a)

Defined in Idris.DeepSeq

Methods

rnf :: Inline a -> ()

type Rep (Inline a)

Defined in Idris.Docstrings

type Rep (Inline a)

parseDocstring :: Text -> Docstring ()

Construct a docstring from a Text that contains Markdown-formatted docs

renderDocstring :: (a -> String -> Doc OutputAnnotation) -> Docstring a -> Doc OutputAnnotation

Convert a docstring to be shown by the pretty-printer

emptyDocstring :: Docstring a

The empty docstring

nullDocstring :: Docstring a -> Bool

Check whether a docstring is emtpy

noDocs :: (Docstring a, [(Name, Docstring a)])

Empty documentation for a definition

overview :: Docstring a -> Docstring a

Construct a docstring consisting of the first block-level element of the argument docstring, for use in summaries.

containsText :: Text -> Docstring a -> Bool

Does a string occur in the docstring?

renderHtml :: Docstring DocTerm -> Html

annotCode

Arguments

:: (String -> b)

How to annotate code samples

-> Docstring a

-> Docstring b

Annotate the code samples in a docstring

data DocTerm

The various kinds of code samples that can be embedded in docs

Constructors

Unchecked

Checked Term

Example Term

Failing Err

Instances

Show DocTerm

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> DocTerm -> ShowS

show :: DocTerm -> String

showList :: [DocTerm] -> ShowS

Generic DocTerm

Defined in Idris.Docstrings

Associated Types

type Rep DocTerm :: Type -> Type

Methods

from :: DocTerm -> Rep DocTerm x

to :: Rep DocTerm x -> DocTerm

Binary DocTerm

Defined in Idris.IBC

Methods

put :: DocTerm -> Put

get :: Get DocTerm

putList :: [DocTerm] -> Put

NFData DocTerm

Defined in Idris.DeepSeq

Methods

rnf :: DocTerm -> ()

type Rep DocTerm

Defined in Idris.Docstrings

type Rep DocTerm = D1 (MetaData "DocTerm" "Idris.Docstrings" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" False) ((C1 (MetaCons "Unchecked" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Checked" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Term))) :+: (C1 (MetaCons "Example" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Term)) :+: C1 (MetaCons "Failing" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Err))))

renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation

Render a term in the documentation

checkDocstring :: forall a b. (String -> [String] -> String -> a -> b) -> Docstring a -> Docstring b

Run some kind of processing step over code in a Docstring. The code processor gets the language and annotations as parameters, along with the source and the original annotation.