Text.Markdown.Errors

Errors which can be raised by the markdown lexer or parser.

Notes: such errors are not supposed to happen, they are used for debugging
purposes.

Definitions

data MdErrorType : Type

Totality: total
Visibility: public export
Constructors:

LexingError : MdErrorType

ParsingError : MdErrorType

Hint: 

Show MdErrorType

record MdError : Type

  A markdown error including the location of the error.

Totality: total
Visibility: public export
Constructor: 

MkMdError : MdErrorType -> Int -> Int -> String -> MdError

Projections:

.column : MdError -> Int

.errorType : MdError -> MdErrorType

.line : MdError -> Int

.msg : MdError -> String

Hint: 

Show MdError

.errorType : MdError -> MdErrorType

Visibility: public export

errorType : MdError -> MdErrorType

Visibility: public export

.line : MdError -> Int

Visibility: public export

line : MdError -> Int

Visibility: public export

.column : MdError -> Int

Visibility: public export

column : MdError -> Int

Visibility: public export

.msg : MdError -> String

Visibility: public export

msg : MdError -> String

Visibility: public export

fromParsingError : ParsingError tok -> MdError

  Converts a parsing error to a markdown error.

Visibility: export