
  0 | module Language.XML.Name
  1 | 
  2 | import Data.String.Parser
  3 | 
  4 | public export
  5 | data Name = MkName String
  6 | 
  7 | %name Name name
  8 | 
  9 | export
 10 | Show Name where
 11 |     show (MkName n) = n
 12 | 
 13 | export
 14 | Eq Name where
 15 |     MkName n1 == MkName n2 = n1 == n2
 16 | 
 17 | public export
 18 | record QName where
 19 |     constructor MkQName
 20 |     namespacePrefix : Maybe Name
 21 |     localPart : Name
 22 | 
 23 | %name QName name
 24 | 
 25 | export
 26 | Show QName where
 27 |     show (MkQName Nothing localPart) = show localPart
 28 |     show (MkQName (Just namespacePrefix) localPart) = show namespacePrefix ++ ":" ++ show localPart
 29 | 
 30 | export
 31 | Eq QName where
 32 |     n1 == n2 = n1.namespacePrefix == n2.namespacePrefix && n1.localPart == n2.localPart
 33 | 
 34 | public export
 35 | isNameStartChar : Char -> Bool
 36 | isNameStartChar c = isAlpha c || c == '_'
 37 | 
 38 | public export
 39 | isNameChar : Char -> Bool
 40 | isNameChar c = isAlphaNum c || c == '.' || c == '-' || c == '_'
 41 | 
 42 | export
 43 | name : Parser Name
 44 | name = MkName <$> pack <$> [| satisfy isNameStartChar :: many (satisfy isNameChar) |]
 45 | 
 46 | export
 47 | qName : Parser QName
 48 | qName = do
 49 |     n <- name
 50 |     Just localPart <- optional (char ':' *> name)
 51 |         | Nothing => pure $ MkQName Nothing n
 52 |     pure $ MkQName (Just n) localPart
 53 |