0 | module Text.Markdown.Data
  1 |
  2 | import Data.String
  3 | import Data.List
  4 |
  5 | import Internal.String
  6 |
  7 | %default total
  8 |
  9 | public export
 10 | data Inline
 11 |   = Text String
 12 |   | Pre String
 13 |   | CodeBlock String (Maybe String)
 14 |   | Italics (List Inline)
 15 |   | Bold (List Inline)
 16 |   | Link String String
 17 |   | Image String String
 18 |   | Html String (List Inline)
 19 |   | NewLine
 20 |
 21 | public export
 22 | data Block
 23 |    = Header Nat (List Inline)
 24 |    | HorizontalRules
 25 |    | Paragraph (List Inline)
 26 |
 27 | public export
 28 | data Markdown =
 29 |   Doc (List Block)
 30 |
 31 | %name Markdown markdown
 32 |
 33 | mutual
 34 |   covering
 35 |   showInlines : List Inline -> String
 36 |   showInlines = showList showInline
 37 |
 38 |   covering
 39 |   showBlocks : List Block -> String
 40 |   showBlocks = showList showBlock
 41 |
 42 |   covering
 43 |   showBlock : Block -> String
 44 |   showBlock (Header level inline) = "H" ++ (show level) ++ " " ++ (showInlines inline)
 45 |   showBlock (HorizontalRules) = "HR"
 46 |   showBlock (Paragraph inline) = "P " ++ (showInlines inline)
 47 |
 48 |   covering
 49 |   showInline : Inline -> String
 50 |   showInline (Text text) = "Text " ++ (quote text)
 51 |   showInline (Pre text) = "Pre " ++ (quote text)
 52 |   showInline (CodeBlock text type) = "CodeBlock [" ++ show type ++ "] " ++ (quote text)
 53 |   showInline (Italics inline) = "Italics " ++ (showInlines inline)
 54 |   showInline (Bold inline) = "Bold " ++ (showInlines inline)
 55 |   showInline (Link href desc) = "Link " ++ href ++ " " ++ desc
 56 |   showInline (Image alt src) = "Image " ++ alt ++ " " ++ src
 57 |   showInline (Html tag inline) = "HTML <" ++ tag ++ "> " ++ (showInlines inline)
 58 |   showInline NewLine = "NewLine"
 59 |
 60 | export
 61 | covering
 62 | Show Inline where
 63 |   show = showInline
 64 |
 65 | export
 66 | covering
 67 | Show Block where
 68 |   show = showBlock
 69 |
 70 | export
 71 | covering
 72 | Show Markdown where
 73 |   show (Doc blocks) = showBlocks blocks
 74 |
 75 | export
 76 | covering
 77 | Eq Inline where
 78 |   (Text text0) == (Text text1) = text0 == text1
 79 |   (Pre text0) == (Pre text1) = text0 == text1
 80 |   (CodeBlock text0 type0) == (CodeBlock text1 type1) = text0 == text1 && type0 == type1
 81 |   (Italics inline0) == (Italics inline1) = inline0 == inline1
 82 |   (Bold inline0) == (Bold inline1) = inline0 == inline1
 83 |   (Link href0 desc0) == (Link href1 desc1) = href0 == href1 && desc0 == desc1
 84 |   (Image href0 desc0) == (Image href1 desc1) = href0 == href1 && desc0 == desc1
 85 |   (Html tag0 inline0) == (Html tag1 inline1) = tag0 == tag1 && inline0 == inline1
 86 |   NewLine == NewLine = True
 87 |   _ == _ = False
 88 |
 89 | export
 90 | covering
 91 | Eq Block where
 92 |   (Header level0 inline0) == (Header level1 inline1) = level0 == level1 && inline0 == inline1
 93 |   HorizontalRules == HorizontalRules = True
 94 |   (Paragraph inline0) == (Paragraph inline1) = inline0 == inline1
 95 |   _ == _ = False
 96 |
 97 | export
 98 | covering
 99 | Eq Markdown where
100 |   (Doc a) == (Doc b) = a == b
101 |