Idris2Doc : Text.Markdown.String

Text.Markdown.String

(source)

Definitions

blankLines : Lexer
  One or more blank lines which may contain spaces.

Totality: total
Visibility: export
headingSym : Lexer
Totality: total
Visibility: export
uListSym : Lexer
  A list symbol '-' followed by one space.

Totality: total
Visibility: export
uListSepSym : Lexer
  A list symbol '-' preceded by a newline and followed by one space.

This token can then be used as list items separators consuming the newline.

Totality: total
Visibility: export
horizontalRules : Lexer
  A horizontal rule.

The horizontal rule is represented by three or more consecutive '*', '-', or
'_' characters.

A blank line should be placed before and after the horizontal rule, unless
at the end of the beginning or end of the text.

```markdown
Hello

---

World
```

Totality: total
Visibility: export
openingBracket : Lexer
  An opening bracket `[`

Totality: total
Visibility: export
closingBracket : Lexer
  A closing bracket `]`.

Totality: total
Visibility: export
openingParenthesis : Lexer
  An opening parenthesis `(`.

Totality: total
Visibility: export
closingParenthesis : Lexer
  A closing parenthesis `)`.

Totality: total
Visibility: export
imageStart : Lexer
  Start of an image `![`.

Totality: total
Visibility: export
italicsSym : Lexer
Totality: total
Visibility: export
boldSym : Lexer
Totality: total
Visibility: export
htmlOpenTag : Lexer
  Note: we currently don't allow attributes
To do so, we might need to move this from the lexer into the parser

Totality: total
Visibility: export
htmlCloseTag : Lexer
Totality: total
Visibility: export
pre : Lexer
Totality: total
Visibility: export
code : Lexer
  A code block between two code fences "```" or "~~~".

Totality: total
Visibility: export
text : Lexer
  Consumes anything but the other lexers.

Totality: total
Visibility: export