
  0 | module Language.XML.CharData
  1 | 
  2 | import public Data.List
  3 | import public Data.String
  4 | import Data.String.Extra
  5 | import Data.String.Parser
  6 | 
  7 | public export
  8 | record CharData where
  9 |     constructor MkCharData
 10 |     preSpace : Bool
 11 |     c : String
 12 |     postSpace : Bool
 13 | 
 14 | %name CharData c, d
 15 | 
 16 | public export
 17 | maybeSpace : Bool -> String
 18 | maybeSpace False = ""
 19 | maybeSpace True = " "
 20 | 
 21 | export
 22 | Show CharData where
 23 |     show (MkCharData preSpace c postSpace) = maybeSpace preSpace ++ c ++ maybeSpace postSpace
 24 | 
 25 | public export
 26 | fromString : String -> CharData
 27 | fromString str = case unpack str of
 28 |     [] => MkCharData False "" False
 29 |     cs@(_ :: _) =>
 30 |         let s = trim str in
 31 |         MkCharData (isSpace $ head cs) s ((not $ null s) && (isSpace $ last cs))
 32 | 
 33 | public export
 34 | (++) : CharData -> CharData -> CharData
 35 | (MkCharData preSpace "" midLeftSpace) ++ (MkCharData midRightSpace d postSpace) =
 36 |     MkCharData (preSpace || midLeftSpace || midRightSpace) d postSpace
 37 | (MkCharData preSpace c midLeftSpace) ++ (MkCharData midRightSpace "" postSpace) =
 38 |     MkCharData preSpace c (midLeftSpace || midRightSpace || postSpace)
 39 | (MkCharData preSpace c midLeftSpace) ++ (MkCharData midRightSpace d postSpace) =
 40 |     MkCharData preSpace (c ++ maybeSpace (midLeftSpace || midRightSpace) ++ d) postSpace
 41 | 
 42 | public export
 43 | Semigroup CharData where
 44 |     (<+>) = (++)
 45 | 
 46 | public export
 47 | Monoid CharData where
 48 |     neutral = ""
 49 | 
 50 | export
 51 | charData : Parser CharData
 52 | charData = do
 53 |     let word = map pack $ some $ satisfy $ \c => not (isSpace c) && c /= '<'
 54 | 
 55 |     preSpace <- succeeds spaces1
 56 |     words <- (many $ spaces *> word)
 57 |     postSpace <- succeeds spaces1
 58 | 
 59 |     pure $ MkCharData preSpace (join " " words) postSpace
 60 |