0 | module Text.Markdown.Tokens
  1 |
  2 | import Data.String
  3 | import Data.String.Extra
  4 | import Text.Markdown.String
  5 | import Internal.String
  6 | import public Text.Token
  7 |
  8 | %default total
  9 |
 10 | safeSub : Nat -> Nat -> Nat
 11 | safeSub _ Z = Z
 12 | safeSub Z v = v
 13 | safeSub (S n) (S k) = safeSub n k
 14 |
 15 | getLinkDesc : String -> (String, String)
 16 | getLinkDesc text =
 17 |   let
 18 |     (linkPart, descPart) = break (== ']') text
 19 |     linkLenFinal = safeSub 1 (length linkPart)
 20 |     descLenFinal = safeSub 3 (length descPart)
 21 |   in
 22 |     (
 23 |       substr 1 linkLenFinal linkPart,
 24 |       substr 2 descLenFinal descPart
 25 |     )
 26 |
 27 | public export
 28 | data MarkdownTokenKind
 29 |   = BlankLine
 30 |   | HeadingSym
 31 |   | MdText
 32 |   | MdPre
 33 |   | MdCodeBlock
 34 |   | MdHorizontalRules
 35 |   | MdNewLine
 36 |   | ItalicsSym
 37 |   | BoldSym
 38 |   | ImageSym
 39 |   | MdLink
 40 |   | HtmlOpenTag
 41 |   | HtmlCloseTag
 42 |
 43 | public export
 44 | Eq MarkdownTokenKind where
 45 |   (==) BlankLine BlankLine = True
 46 |   (==) HeadingSym HeadingSym = True
 47 |   (==) MdText MdText = True
 48 |   (==) MdPre MdPre = True
 49 |   (==) MdCodeBlock MdCodeBlock = True
 50 |   (==) MdHorizontalRules MdHorizontalRules = True
 51 |   (==) MdNewLine MdNewLine = True
 52 |   (==) ItalicsSym ItalicsSym = True
 53 |   (==) BoldSym BoldSym = True
 54 |   (==) ImageSym ImageSym = True
 55 |   (==) MdLink MdLink = True
 56 |   (==) HtmlOpenTag HtmlOpenTag = True
 57 |   (==) HtmlCloseTag HtmlCloseTag = True
 58 |   (==) _ _ = False
 59 |
 60 | public export
 61 | MarkdownToken : Type
 62 | MarkdownToken = Token MarkdownTokenKind
 63 |
 64 | dropEnds : Int -> String -> String
 65 | dropEnds n str =
 66 |   let
 67 |     len : Int
 68 |     len = cast $ length str
 69 |   in
 70 |     strSubstr n (len - 2 * n) str
 71 |
 72 | public export
 73 | TokenKind MarkdownTokenKind where
 74 |   TokType BlankLine = ()
 75 |   TokType HeadingSym = Nat
 76 |   TokType MdText = String
 77 |   TokType MdPre = String
 78 |   TokType MdCodeBlock = (String, Maybe String)
 79 |   TokType MdHorizontalRules = ()
 80 |   TokType MdNewLine = ()
 81 |   TokType ItalicsSym = ()
 82 |   TokType BoldSym = ()
 83 |   TokType ImageSym = ()
 84 |   TokType MdLink = (String, String)
 85 |   TokType HtmlOpenTag = String
 86 |   TokType HtmlCloseTag = String
 87 |
 88 |   tokValue BlankLine _ = ()
 89 |   tokValue HeadingSym x = length x
 90 |   tokValue MdText txt = txt
 91 |   tokValue MdPre txt = dropEnds 1 txt
 92 |   tokValue MdCodeBlock txt =
 93 |     case Internal.String.split '\n' (dropEnds 3 txt) of
 94 |       [] =>
 95 |         ("", Nothing)
 96 |
 97 |       ("\n" :: x) =>
 98 |         (join "\n" x, Nothing)
 99 |
100 |       hd :: x =>
101 |         (join "\n" x, Just hd)
102 |
103 |   tokValue MdHorizontalRules _ = ()
104 |   tokValue MdNewLine _ = ()
105 |   tokValue ItalicsSym _ = ()
106 |   tokValue BoldSym _ = ()
107 |   tokValue ImageSym _ = ()
108 |   tokValue MdLink text = getLinkDesc text
109 |   tokValue HtmlOpenTag tag = (filter isAlphaNum tag) -- TODO: Improve quality
110 |   tokValue HtmlCloseTag tag = (filter isAlphaNum tag) -- how to do this?
111 |
112 | export
113 | partial
114 | Show MarkdownToken where
115 |   show (Tok BlankLine _) = "BlankLine"
116 |   show (Tok HeadingSym l) = "HeadingSym " ++ (show l)
117 |   show (Tok MdText txt) = "MdText " ++ (quote txt)
118 |   show (Tok MdPre txt) = "MdPre " ++ (quote txt)
119 |   show (Tok MdCodeBlock txt) = "MdCodeBlock " ++ (quote txt)
120 |   show (Tok MdHorizontalRules _) = "MdHorizontalRules"
121 |   show (Tok MdNewLine _) = "MdNewLine"
122 |   show (Tok ItalicsSym _) = "ItalicsSym"
123 |   show (Tok BoldSym _) = "BoldSym"
124 |   show (Tok ImageSym _) = "ImageSym"
125 |   show (Tok MdLink txt) = "MdLink " ++ (quote txt)
126 |   show (Tok HtmlOpenTag tag) = "StartTag " ++ quote tag
127 |   show (Tok HtmlCloseTag tag) = "EndTag " ++ quote tag
128 |
129 | export
130 | Eq MarkdownToken where
131 |   (Tok BlankLine _) == (Tok BlankLine _) = True
132 |   (Tok HeadingSym l0) == (Tok HeadingSym l1) = l0 == l1
133 |   (Tok MdText txt0) == (Tok MdText txt1) = txt0 == txt1
134 |   (Tok MdPre txt0) == (Tok MdPre txt1) = txt0 == txt1
135 |   (Tok MdCodeBlock txt0) == (Tok MdCodeBlock txt1) = txt0 == txt1
136 |   (Tok MdHorizontalRules _) == (Tok MdHorizontalRules _) = True
137 |   (Tok MdNewLine _) == (Tok MdNewLine _) = True
138 |   (Tok ItalicsSym _) == (Tok ItalicsSym _) = True
139 |   (Tok BoldSym _) == (Tok BoldSym _) = True
140 |   (Tok ImageSym _) == (Tok ImageSym _) = True
141 |   (Tok MdLink txt0) == (Tok MdLink txt1) = txt0 == txt1
142 |   (Tok HtmlOpenTag tag0) == (Tok HtmlOpenTag tag1) = tag0 == tag1
143 |   (Tok HtmlCloseTag tag0) == (Tok HtmlCloseTag tag1) = tag0 == tag1
144 |   _ == _ = False
145 |