idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
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
Functor Docstring Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

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

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)

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 -> ()

Generic (Docstring a) Source # 
Instance details

Defined in Idris.Docstrings

Associated Types

type Rep (Docstring a) 
Instance details

Defined in Idris.Docstrings

type Rep (Docstring a)

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

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
Functor Block Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

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

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)

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 -> ()

Generic (Block a) Source # 
Instance details

Defined in Idris.Docstrings

Associated Types

type Rep (Block a) 
Instance details

Defined in Idris.Docstrings

type Rep (Block a)

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

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
Functor Inline Source # 
Instance details

Defined in Idris.Docstrings

Methods

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

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

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)

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 -> ()

Generic (Inline a) Source # 
Instance details

Defined in Idris.Docstrings

Associated Types

type Rep (Inline a) 
Instance details

Defined in Idris.Docstrings

type Rep (Inline a)

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

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?

renderHtml :: Docstring DocTerm -> Html Source #

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

Constructors

Unchecked 
Checked Term 
Example Term 
Failing Err 

Instances

Instances details
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 -> ()

Generic DocTerm Source # 
Instance details

Defined in Idris.Docstrings

Associated Types

type Rep DocTerm 
Instance details

Defined in Idris.Docstrings

type Rep DocTerm = D1 ('MetaData "DocTerm" "Idris.Docstrings" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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))))

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

type Rep DocTerm Source # 
Instance details

Defined in Idris.Docstrings

type Rep DocTerm = D1 ('MetaData "DocTerm" "Idris.Docstrings" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" '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 :: (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.