idris-0.11.1: Functional Programming Language with Dependent Types

Safe HaskellNone



Wrapper around Markdown library



data Docstring a Source

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


DocString Options (Blocks a) 

data Block a Source

Block-level elements.


Para (Inlines a) 
Header Int (Inlines a) 
Blockquote (Blocks a) 
List Bool ListType [Blocks a] 
CodeBlock CodeAttr Text a 
HtmlBlock Text 

data Inline a Source


Str Text 
Emph (Inlines a) 
Strong (Inlines a) 
Code Text a 
Link (Inlines a) Text Text 
Image (Inlines a) Text Text 
Entity Text 
RawHtml Text 

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


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


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.