0 | module Text.Markdown.String
  1 |
  2 | import Data.Nat
  3 | import Text.Lexer
  4 | import Text.Quantity
  5 |
  6 | %default total
  7 |
  8 | ||| End of the file, no more character to consume.
  9 | private
 10 | eof : Recognise False
 11 | eof = reject any
 12 |
 13 | ||| End of a block, which may be a blank line or the end of the file.
 14 | private
 15 | blockEnd : Recognise False
 16 | blockEnd =
 17 |       (newline <+> manyUntil newline space <+> newline)
 18 |   <|> (some newline <+> eof)
 19 |   <|> eof
 20 |
 21 | ||| One or more blank lines which may contain spaces.
 22 | export
 23 | blankLines : Lexer
 24 | blankLines = newline <+> manyThen newlines space
 25 |
 26 | export
 27 | headingSym : Lexer
 28 | headingSym = some (is '#')
 29 |
 30 | ||| A list symbol '-' followed by one space.
 31 | export
 32 | uListSym : Lexer
 33 | uListSym = is '-' <+> space
 34 |
 35 | ||| A list symbol '-' preceded by a newline and followed by one space.
 36 | |||
 37 | ||| This token can then be used as list items separators consuming the newline.
 38 | export
 39 | uListSepSym : Lexer
 40 | uListSepSym = newline <+> is '-' <+> space
 41 |
 42 | ||| A horizontal rule.
 43 | |||
 44 | ||| The horizontal rule is represented by three or more consecutive '*', '-', or
 45 | ||| '_' characters.
 46 | |||
 47 | ||| A blank line should be placed before and after the horizontal rule, unless
 48 | ||| at the end of the beginning or end of the text.
 49 | |||
 50 | ||| ```markdown
 51 | ||| Hello
 52 | |||
 53 | ||| ---
 54 | |||
 55 | ||| World
 56 | ||| ```
 57 | export
 58 | horizontalRules : Lexer
 59 | horizontalRules = (atLeast3 '*' <|> atLeast3 '-' <|> atLeast3 '_') <+> blockEnd
 60 |   where
 61 |     atLeast3 : Char -> Lexer
 62 |     atLeast3 c = is c <+> is c <+> some (is c)
 63 |
 64 | ||| An opening bracket `[`
 65 | export
 66 | openingBracket : Lexer
 67 | openingBracket = is '['
 68 |
 69 | ||| A closing bracket `]`.
 70 | export
 71 | closingBracket : Lexer
 72 | closingBracket = is ']'
 73 |
 74 | ||| An opening parenthesis `(`.
 75 | export
 76 | openingParenthesis : Lexer
 77 | openingParenthesis = is '('
 78 |
 79 | ||| A closing parenthesis `)`.
 80 | export
 81 | closingParenthesis : Lexer
 82 | closingParenthesis = is ')'
 83 |
 84 | ||| Start of an image `![`.
 85 | export
 86 | imageStart : Lexer
 87 | imageStart = is '!' <+> openingBracket
 88 |
 89 | export
 90 | italicsSym : Lexer
 91 | italicsSym = is '_'
 92 |
 93 | export
 94 | boldSym : Lexer
 95 | boldSym = count (exactly 2) (is '*')
 96 |
 97 | ||| Note: we currently don't allow attributes
 98 | ||| To do so, we might need to move this from the lexer into the parser
 99 | export
100 | htmlOpenTag : Lexer
101 | htmlOpenTag = surround (is '<') (is '>') alphaNum
102 |
103 | export
104 | htmlCloseTag : Lexer
105 | htmlCloseTag = surround (exact "</") (is '>') alphaNum
106 |
107 | export
108 | pre : Lexer
109 | pre = is '`' <+> some (non (newline <|> is '`')) <+> is '`'
110 |
111 | ||| A code fence of defined as "```" or "~~~".
112 | private
113 | codeFence : Lexer
114 | codeFence = count (exactly 3) (is '`') <|> count (exactly 3) (is '~')
115 |
116 | ||| The end of a code block.
117 | private
118 | codeEnd : Lexer
119 | codeEnd = newline <+> codeFence <+> blockEnd
120 |
121 | ||| A code block between two code fences "```" or "~~~".
122 | export
123 | code : Lexer
124 | code = codeFence <+> many (alphaNum) <+> newline <+> manyThen codeEnd any
125 |
126 | ||| Consumes anything but the other lexers.
127 | export
128 | text : Lexer
129 | text = some $ non $ choice
130 |   [ code
131 |   , imageStart
132 |   , openingBracket
133 |   , closingBracket
134 |   , openingParenthesis
135 |   , closingParenthesis
136 |   , italicsSym
137 |   , boldSym
138 |   , htmlOpenTag
139 |   , htmlCloseTag
140 |   , pre
141 |   , blankLines
142 |   , newlines
143 |   ]
144 |