0 | module Language.XML.Element
  1 |
  2 | import Data.Either
  3 | import Data.List1
  4 | import public Data.List.Alternating
  5 | import Data.String
  6 | import Data.String.Extra
  7 | import Data.String.Parser
  8 |
  9 | import public Language.XML.Attribute
 10 | import public Language.XML.CharData
 11 | import public Language.XML.Misc
 12 | import public Language.XML.Name
 13 |
 14 | public export
 15 | data Element = EmptyElem QName (List Attribute)
 16 |              | Elem QName (List Attribute) (Odd CharData $ Either Misc Element)
 17 |
 18 | %name Element elem
 19 |
 20 | public export
 21 | (.name) : Element -> QName
 22 | (EmptyElem name _).name = name
 23 | (Elem name _ _).name = name
 24 |
 25 | public export
 26 | (.attrs) : Element -> List Attribute
 27 | (EmptyElem _ attrs).attrs = attrs
 28 | (Elem _ attrs _).attrs = attrs
 29 |
 30 | public export
 31 | (.content) : Element -> Odd CharData (Either Misc Element)
 32 | (EmptyElem _ _).content = [""]
 33 | (Elem _ _ content).content = content
 34 |
 35 | public export
 36 | maybeNl : Bool -> String
 37 | maybeNl False = ""
 38 | maybeNl True = "\n"
 39 |
 40 | public export
 41 | showNl : CharData -> String
 42 | showNl (MkCharData preSpace c postSpace) = maybeNl preSpace ++ c ++ maybeNl postSpace
 43 |
 44 | public export
 45 | textContent : Element -> String
 46 | textContent (EmptyElem name attrs) = ""
 47 | textContent (Elem name attrs content) = concat $ Odd.forget $
 48 |     bimap showNl textContent $ content >>= either (const neutral) pure
 49 |
 50 | public export
 51 | find : (Element -> Bool) -> Element -> Maybe Element
 52 | find f elem = find f (rights $ evens elem.content)
 53 |
 54 | public export
 55 | mapContent : (Odd CharData (Either Misc Element) -> Odd CharData (Either Misc Element)) -> Element -> Element
 56 | mapContent f (EmptyElem name attrs) = EmptyElem name attrs
 57 | mapContent f (Elem name attrs content) = Elem name attrs (f content)
 58 |
 59 | public export
 60 | mapContentM : Monad m => (Odd CharData (Either Misc Element) -> m (Odd CharData (Either Misc Element))) -> Element -> m Element
 61 | mapContentM f (EmptyElem name attrs) = pure $ EmptyElem name attrs
 62 | mapContentM f (Elem name attrs content) = pure $ Elem name attrs !(f content)
 63 |
 64 | indentTail : String -> String
 65 | indentTail str =
 66 |     let (x ::: xs) = split (== '\n') str in
 67 |     join "\n" (x :: map indent xs)
 68 |   where
 69 |     indent : String -> String
 70 |     indent "" = ""
 71 |     indent s = "    " ++ s
 72 |
 73 | export
 74 | Show Element where
 75 |     show (EmptyElem name attrs) =
 76 |         "<\{show name}\{concat $ map (\attr => " " ++ show attr) attrs}/>"
 77 |     show (Elem name attrs content) =
 78 |         """
 79 |         <\{show name}\{concat $ map (\attr => " " ++ show attr) attrs}>\
 80 |         \{indentTail $ concat $ forget $ assert_total $ bimap showNl (either show show) content}\
 81 |         </\{show name}>
 82 |         """
 83 |
 84 | export
 85 | element : Parser Element
 86 | element = (do
 87 |     ignore $ string "<"
 88 |     name <- qName
 89 |     attrs <- many (spaces *> attribute)
 90 |     spaces
 91 |     Nothing <- optional $ string "/>"
 92 |         | Just _ => pure $ EmptyElem name attrs
 93 |     ignore $ string ">"
 94 |
 95 |     content <- alternating charData $ map Left misc <|> map Right element
 96 |
 97 |     string "</\{show name}" *> spaces <* string ">"
 98 |
 99 |     pure $ Elem name attrs content
100 |   ) <?> "XML element"
101 |