Text.Markdown.Data

Definitions

data Inline : Type

Totality: total
Visibility: public export
Constructors:

Text : String -> Inline

Pre : String -> Inline

Italics : List Inline -> Inline

Bold : List Inline -> Inline

Link : List Inline -> String -> Inline

Image : String -> String -> Inline

Html : String -> List Inline -> Inline

Hints:

Eq Inline

Show Inline

ListItem : Type

Totality: total
Visibility: public export

data Block : Type

Totality: total
Visibility: public export
Constructors:

Header : Nat -> List Inline -> Block

UList : List ListItem -> Block

CodeBlock : String -> Maybe String -> Block

HorizontalRules : Block

Paragraph : List Inline -> Block

Hints:

Eq Block

Show Block

data Markdown : Type

Totality: total
Visibility: public export
Constructor: 

Doc : List Block -> Markdown

Hints:

Eq Markdown

Show Markdown

concatInlineVals : List Inline -> String

  Concatenate a list of inline values to a single string.

Totality: total
Visibility: export

normalise : Markdown -> Markdown

  Concatenates the successive `Text` within inline elements.
  
  The parser may return successive `Text`. For example: "Hello world!" will
  be parsed with two `Text`: "Hello world" and "!". The goal of this function
  is to normalise it to "Hello world!".

Totality: total
Visibility: export