idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Docstrings

Description

 
Synopsis

Documentation

data Docstring a Source #

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

Instances details
Foldable Docstring Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

foldMap :: Monoid m => (a -> m) -> Docstring a -> 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 Source # 
Instance details

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)

Functor Docstring Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

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

Generic (Docstring a) Source # 
Instance details

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

Show a => Show (Docstring a) Source # 
Instance details

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> Docstring a -> ShowS

show :: Docstring a -> String

showList :: [Docstring a] -> ShowS

Binary a => Binary (Docstring a) 
Instance details

Defined in Idris.IBC

Methods

put :: Docstring a -> Put

get :: Get (Docstring a)

putList :: [Docstring a] -> Put

NFData a => NFData (Docstring a) 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Docstring a -> ()

type Rep (Docstring a) Source # 
Instance details

Defined in Idris.Docstrings

type Rep (Docstring a)

data Block a Source #

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

Instances details
Foldable Block Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

foldMap :: Monoid m => (a -> m) -> Block a -> 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 Source # 
Instance details

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)

Functor Block Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

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

Generic (Block a) Source # 
Instance details

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

Show a => Show (Block a) Source # 
Instance details

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> Block a -> ShowS

show :: Block a -> String

showList :: [Block a] -> ShowS

Binary a => Binary (Block a) 
Instance details

Defined in Idris.IBC

Methods

put :: Block a -> Put

get :: Get (Block a)

putList :: [Block a] -> Put

NFData a => NFData (Block a) 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Block a -> ()

type Rep (Block a) Source # 
Instance details

Defined in Idris.Docstrings

type Rep (Block a)

data Inline a Source #

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

Instances details
Foldable Inline Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

foldMap :: Monoid m => (a -> m) -> Inline a -> 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 Source # 
Instance details

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)

Functor Inline Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

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

Generic (Inline a) Source # 
Instance details

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

Show a => Show (Inline a) Source # 
Instance details

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> Inline a -> ShowS

show :: Inline a -> String

showList :: [Inline a] -> ShowS

Binary a => Binary (Inline a) 
Instance details

Defined in Idris.IBC

Methods

put :: Inline a -> Put

get :: Get (Inline a)

putList :: [Inline a] -> Put

NFData a => NFData (Inline a) 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: Inline a -> ()

type Rep (Inline a) Source # 
Instance details

Defined in Idris.Docstrings

type Rep (Inline a)

parseDocstring :: Text -> Docstring () Source #

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

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

Convert a docstring to be shown by the pretty-printer

emptyDocstring :: Docstring a Source #

The empty docstring

nullDocstring :: Docstring a -> Bool Source #

Check whether a docstring is emtpy

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

Empty documentation for a definition

overview :: Docstring a -> Docstring a Source #

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

containsText :: Text -> Docstring a -> Bool Source #

Does a string occur in the docstring?

annotCode Source #

Arguments

:: forall a b. (String -> b)

How to annotate code samples

-> Docstring a 
-> Docstring b 

Annotate the code samples in a docstring

data DocTerm Source #

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

Instances

Instances details
Generic DocTerm Source # 
Instance details

Defined in Idris.Docstrings

Associated Types

type Rep DocTerm :: Type -> Type

Methods

from :: DocTerm -> Rep DocTerm x

to :: Rep DocTerm x -> DocTerm

Show DocTerm Source # 
Instance details

Defined in Idris.Docstrings

Methods

showsPrec :: Int -> DocTerm -> ShowS

show :: DocTerm -> String

showList :: [DocTerm] -> ShowS

Binary DocTerm 
Instance details

Defined in Idris.IBC

Methods

put :: DocTerm -> Put

get :: Get DocTerm

putList :: [DocTerm] -> Put

NFData DocTerm 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: DocTerm -> ()

type Rep DocTerm Source # 
Instance details

Defined in Idris.Docstrings

type Rep DocTerm = D1 ('MetaData "DocTerm" "Idris.Docstrings" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" '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 Source #

Render a term in the documentation

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

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.