0 | module Text.Markdown.Tokens
  1 |
  2 | import Data.String
  3 |
  4 | import Data.String.Extra
  5 | import Derive.Prelude
  6 |
  7 | import Text.Markdown.String
  8 | import public Text.Token
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | public export
 14 | data MarkdownTokenKind
 15 |   = BlankLine
 16 |   | HeadingSym
 17 |   | UListSym
 18 |   | UListSepSym
 19 |   | MdText
 20 |   | MdPre
 21 |   | MdCodeBlock
 22 |   | MdHorizontalRules
 23 |   | MdNewLine
 24 |   | ItalicsSym
 25 |   | BoldSym
 26 |   | ImageStart
 27 |   | OpeningBracket
 28 |   | ClosingBracket
 29 |   | OpeningParenthesis
 30 |   | ClosingParenthesis
 31 |   | HtmlOpenTag
 32 |   | HtmlCloseTag
 33 |
 34 | %runElab derive "MarkdownTokenKind" [Eq, Show]
 35 |
 36 | public export
 37 | MarkdownToken : Type
 38 | MarkdownToken = Token MarkdownTokenKind
 39 |
 40 | %runElab derive "Token" [Eq, Show]
 41 |
 42 | ||| Drop both ends of a string.
 43 | |||
 44 | ||| This is a combination of `drop` and `dropLast`.
 45 | private
 46 | dropEnds : Nat -> String -> String
 47 | dropEnds n = drop n . dropLast n
 48 |
 49 | ||| Drops the last element of a list.
 50 | |||
 51 | ||| Note: this function doesn't seem to be present in base nor contrib.
 52 | private
 53 | dropLast : List a -> List a
 54 | dropLast []        = []
 55 | dropLast (x :: []) = []
 56 | dropLast (x :: xs) = x :: dropLast xs
 57 |
 58 | public export
 59 | TokenKind MarkdownTokenKind where
 60 |   TokType BlankLine          = ()
 61 |   TokType HeadingSym         = Nat
 62 |   TokType UListSym           = String
 63 |   TokType UListSepSym        = String
 64 |   TokType MdText             = String
 65 |   TokType MdPre              = String
 66 |   TokType MdCodeBlock        = (String, Maybe String)
 67 |   TokType MdHorizontalRules  = ()
 68 |   TokType MdNewLine          = ()
 69 |   TokType ItalicsSym         = String
 70 |   TokType BoldSym            = String
 71 |   TokType ImageStart         = String
 72 |   TokType OpeningBracket     = String
 73 |   TokType ClosingBracket     = String
 74 |   TokType OpeningParenthesis = String
 75 |   TokType ClosingParenthesis = String
 76 |   TokType HtmlOpenTag        = String
 77 |   TokType HtmlCloseTag       = String
 78 |
 79 |   tokValue BlankLine _          = ()
 80 |   tokValue HeadingSym x         = length x
 81 |   tokValue UListSym txt         = txt
 82 |   tokValue UListSepSym txt      = txt
 83 |   tokValue MdText txt           = txt
 84 |   tokValue MdPre txt            = dropEnds 1 txt
 85 |   tokValue MdCodeBlock txt      =
 86 |     let ls = lines txt in
 87 |     ( dropLast 1 $ unlines $ dropLast $ drop 1 ls
 88 |     , rtrim . drop 3 <$> head' ls
 89 |     )
 90 |
 91 |   tokValue MdHorizontalRules _    = ()
 92 |   tokValue MdNewLine _            = ()
 93 |   tokValue ItalicsSym txt         = txt
 94 |   tokValue BoldSym txt            = txt
 95 |   tokValue ImageStart txt         = txt
 96 |   tokValue OpeningBracket txt     = txt
 97 |   tokValue ClosingBracket txt     = txt
 98 |   tokValue OpeningParenthesis txt = txt
 99 |   tokValue ClosingParenthesis txt = txt
100 |   tokValue HtmlOpenTag tag        = dropEnds 1 tag
101 |   tokValue HtmlCloseTag tag       = dropLast 1 (drop 2 tag)
102 |