
   0 | module Text.Markdown.Data
   1 | 
   2 | import Data.String
   3 | import Data.List
   4 | 
   5 | import Derive.Prelude
   6 | 
   7 | %default total
   8 | %language ElabReflection
   9 | 
  10 | public export
  11 | data Inline
  12 |   = Text String
  13 |   | Pre String
  14 |   | Italics (List Inline)
  15 |   | Bold (List Inline)
  16 |   | Link (List Inline) String
  17 |   | Image String String
  18 |   | Html String (List Inline)
  19 | 
  20 | %runElab derive "Inline" [Eq, Show]
  21 | 
  22 | public export
  23 | ListItem : Type
  24 | ListItem = List Inline
  25 | 
  26 | public export
  27 | data Block
  28 |    = Header Nat (List Inline)
  29 |    | UList (List ListItem)
  30 |    | CodeBlock String (Maybe String)
  31 |    | HorizontalRules
  32 |    | Paragraph (List Inline)
  33 | 
  34 | %runElab derive "Block" [Eq, Show]
  35 | 
  36 | public export
  37 | data Markdown =
  38 |   Doc (List Block)
  39 | 
  40 | %runElab derive "Markdown" [Eq, Show]
  41 | 
  42 | %name Markdown markdown
  43 | 
  44 | ||| Concatenate a list of inline values to a single string.
  45 | export
  46 | concatInlineVals : List Inline -> String
  47 | concatInlineVals []        = ""
  48 | concatInlineVals (x :: xs) = inlineValue x <+> concatInlineVals xs
  49 |   where
  50 |     inlineValue : Inline -> String
  51 |     inlineValue (Text txt)        = txt
  52 |     inlineValue (Pre txt)         = txt
  53 |     inlineValue (Italics inlines) = concatInlineVals inlines
  54 |     inlineValue (Bold inlines)    = concatInlineVals inlines
  55 |     inlineValue (Link inlines _)  = concatInlineVals inlines
  56 |     inlineValue (Image alt _)     = alt
  57 |     inlineValue (Html _ inlines)  = concatInlineVals inlines
  58 | 
  59 | ||| Concatenates the successive `Text` within inline elements.
  60 | |||
  61 | ||| The parser may return successive `Text`. For example: "Hello world!" will
  62 | ||| be parsed with two `Text`: "Hello world" and "!". The goal of this function
  63 | ||| is to normalise it to "Hello world!".
  64 | export
  65 | normalise : Markdown -> Markdown
  66 | normalise (Doc blocks) = Doc (map normBlockTexts blocks)
  67 |   where
  68 |     normInlineTexts : List Inline -> List Inline
  69 |     normInlineTexts []                             = []
  70 |     normInlineTexts (Italics inlines :: xs)        =
  71 |       Italics (normInlineTexts inlines) :: normInlineTexts xs
  72 | 
  73 |     normInlineTexts (Bold inlines :: xs)           =
  74 |       Bold (normInlineTexts inlines) :: normInlineTexts xs
  75 | 
  76 |     normInlineTexts (Link inlines str :: xs)       =
  77 |       Link (normInlineTexts inlines) str :: normInlineTexts xs
  78 | 
  79 |     normInlineTexts (Html str inlines :: xs)       =
  80 |       Html str (normInlineTexts inlines) :: normInlineTexts xs
  81 | 
  82 |     normInlineTexts (Text txt1 :: Text txt2 :: xs) =
  83 |       assert_total $ normInlineTexts (Text (txt1 <+> txt2) :: xs)
  84 | 
  85 |     normInlineTexts (x :: xs)                      = x :: normInlineTexts xs
  86 | 
  87 |     normList : List ListItem -> List ListItem
  88 |     normList [] = []
  89 |     normList (x :: xs) = normInlineTexts x :: normList xs
  90 | 
  91 |     normBlockTexts : Block -> Block
  92 |     normBlockTexts (Header level inlines) =
  93 |       Header level (normInlineTexts inlines)
  94 | 
  95 |     normBlockTexts (UList inlines)        = UList (normList inlines)
  96 |     normBlockTexts (Paragraph inlines)    = Paragraph (normInlineTexts inlines)
  97 |     normBlockTexts block                  = block
  98 | 
  99 | 
 100 |