
  0 | ||| Errors which can be raised by the markdown lexer or parser.
  1 | |||
  2 | ||| Notes: such errors are not supposed to happen, they are used for debugging
  3 | ||| purposes.
  4 | module Text.Markdown.Errors
  5 | 
  6 | import Text.Parser.Core
  7 | 
  8 | public export
  9 | data MdErrorType = LexingError | ParsingError
 10 | 
 11 | public export
 12 | Show MdErrorType where
 13 |   show LexingError  = "Lexing Error"
 14 |   show ParsingError = "Parsing Error"
 15 | 
 16 | ||| A markdown error including the location of the error.
 17 | public export
 18 | record MdError where
 19 |   constructor MkMdError
 20 |   errorType : MdErrorType
 21 |   line   : Int
 22 |   column : Int
 23 |   msg    : String
 24 | 
 25 | public export
 26 | Show MdError where
 27 |   show e =
 28 |         "\{show e.errorType} on line \{show e.line} column \{show e.column} - "
 29 |     <+> "\{e.msg}"
 30 | 
 31 | ||| Converts a parsing error to a markdown error.
 32 | export
 33 | fromParsingError : ParsingError tok -> MdError
 34 | fromParsingError (Error msg Nothing)       = MkMdError ParsingError 1 1 msg
 35 | fromParsingError (Error msg (Just bounds)) = MkMdError
 36 |                                                ParsingError
 37 |                                                bounds.startLine
 38 |                                                bounds.endLine
 39 |                                                msg
 40 |