hextream 0.2.0.0 → 0.3.0.0

raw patch · 21 files changed

+4995/−226 lines, 21 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +1/−1
• hextream.cabal +9/−2
• src/Data/XML/InternalSubset/Parser/High.hs +39/−0
• src/Data/XML/InternalSubset/Parser/Low.hs +80/−0
• src/Data/XML/InternalSubset/Parser/Mid.hs +209/−0
• src/Data/XML/Parser/High.hs +17/−17
• src/Data/XML/Parser/Low.hs +8/−38
• src/Data/XML/Parser/Low/Reference.hs +55/−0
• src/Data/XML/Parser/Mid.hs +9/−32
• src/Data/XML/Parser/Mid/Comment.hs +30/−0
• src/Data/XML/Parser/Mid/Doctype.hs +13/−74
• src/Data/XML/Parser/Mid/ExternalID.hs +58/−0
• src/Data/XML/Parser/Mid/Instruction.hs +35/−0
• test/feed.xml.high.golden +36/−15
• test/feed.xml.mid.golden +84/−47
• test/feed2.xml +132/−0
• test/feed2.xml.high.golden +1570/−0
• test/feed2.xml.mid.golden +2481/−0
• test/sgml.xml +9/−0
• test/sgml.xml.high.golden +49/−0
• test/sgml.xml.mid.golden +71/−0

@@ -4,7 +4,7 @@  Parsers are organized into 3 layers of increasing abstraction level: low, middle and high. Applications will most probably want to rely on the high-level layer. -The library does not define a data type nor parser for a whole XML document. Instead, parsers operate on XML tokens of various sizes, to allow for a usage in a streaming context (e.g. using [`streaming-attoparsec`](https://hackage.haskell.org/package/streaming-attoparsec)).+The library does not define a data type nor parser for a whole XML document. Instead, parsers operate on XML tokens of various sizes, to allow for a usage in a streaming context (e.g. using [`streaming-attoparsec`](https://hackage.haskell.org/package/streaming-attoparsec), [`pipes-attoparsec`](https://hackage.haskell.org/package/pipes-attoparsec) or [`conduit-attoparsec`]()).  The implementation is based on the following specifications: - [Extensible Markup Language (XML) 1.0 (Fifth Edition)](https://www.w3.org/TR/REC-xml/)

@@ -1,7 +1,7 @@ cabal-version:       2.4  name:                hextream-version:             0.2.0.0+version:             0.3.0.0 synopsis:            Streaming-friendly XML parsers description:         Cf README file homepage:            https://github.com/k0ral/hextream@@ -13,7 +13,7 @@ category:            Parsing, XML build-type:          Custom extra-source-files:  README.md, test/*.xml, test/*.golden-tested-with:         GHC <8.10 && >=8.6+tested-with:         GHC <8.12 && >=8.6  source-repository head   type:     git@@ -29,12 +29,19 @@ library   import: common   exposed-modules:+    Data.XML.InternalSubset.Parser.Low+    Data.XML.InternalSubset.Parser.Mid+    Data.XML.InternalSubset.Parser.High     Data.XML.Parser.Low     Data.XML.Parser.Low.Entity     Data.XML.Parser.Low.Name+    Data.XML.Parser.Low.Reference     Data.XML.Parser.Mid     Data.XML.Parser.Mid.Attribute+    Data.XML.Parser.Mid.Comment     Data.XML.Parser.Mid.Doctype+    Data.XML.Parser.Mid.ExternalID+    Data.XML.Parser.Mid.Instruction     Data.XML.Parser.High     Data.XML.Parser.High.AttrParser     Data.XML.Parser.High.NameParser

@@ -0,0 +1,39 @@+-- | High-level parsers for doctype's internal subset, built on top of "Data.XML.InternalSubset.Parser.Mid":+--+-- - comments are ignored+-- - whitespace between tokens is ignored+module Data.XML.InternalSubset.Parser.High where++import           Data.XML.InternalSubset.Parser.Mid as Mid+import           Data.XML.Parser.Low+import           Data.XML.Parser.Mid.Comment+import           Data.XML.Parser.Mid.Instruction+import           Text.Parser.Char+import           Text.Parser.Combinators+++-- | <https://www.w3.org/TR/REC-xml/#NT-intSubset>+data InternalSubset = InternalSubset+  { _elementTypes      :: [ElementType]+  , _attributeLists    :: [AttributeList]+  , _generalEntities   :: [GeneralEntity]+  , _parameterEntities :: [ParameterEntity]+  , _notations         :: [Notation]+  , _instructions      :: [Instruction]+  } deriving(Eq, Ord, Read, Show)++emptyInternalSubset :: InternalSubset+emptyInternalSubset = InternalSubset mempty mempty mempty mempty mempty mempty++-- | <https://www.w3.org/TR/REC-xml/#NT-intSubset>+internalSubset :: CharParsing m => Monad m => m InternalSubset+internalSubset = do+  tokens <- Mid.runTokenParser Mid.anyToken `sepBy` tokenWhitespace+  pure $ foldr insert emptyInternalSubset tokens+  where insert (TokenElementType e) is     = is { _elementTypes = e : _elementTypes is }+        insert (TokenAttributeList a) is   = is { _attributeLists = a : _attributeLists is }+        insert (TokenGeneralEntity g) is   = is { _generalEntities = g : _generalEntities is }+        insert (TokenParameterEntity p) is = is { _parameterEntities = p : _parameterEntities is }+        insert (TokenNotation n) is        = is { _notations = n : _notations is }+        insert (TokenInstruction i) is     = is { _instructions = i : _instructions is }+        insert (TokenComment c) is         = is

@@ -0,0 +1,80 @@+-- | Low-level parsers for doctype's internal subset:+--+-- - parsed tokens are small and may overlap; it is not possible to tokenize doctype internal-subset in a stateless way+-- - parsers are reversible: all formatting details are retained (e.g. whitespacing)+--+-- All documentation examples assume the following setup:+--+-- > :set -XOverloadedStrings+-- > import Data.Attoparsec.ByteString+module Data.XML.InternalSubset.Parser.Low+  ( module Data.XML.Parser.Low.Name+  , module Data.XML.Parser.Low.Reference+  , module Data.XML.InternalSubset.Parser.Low+  ) where++import           Control.Applicative+import           Control.Monad+import           Data.Text                     (Text)+import qualified Data.Text                     as Text+import           Data.XML.Parser.Low.Name+import           Data.XML.Parser.Low.Reference+import           Text.Parser.Char+import           Text.Parser.Combinators++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> import Data.Attoparsec.ByteString++-- | <https://www.w3.org/TR/REC-xml/#NT-EntityValue>+data EntityValue = ValueText Text | ValueParameterEntityRef ParameterEntityRef | ValueReference Reference+  deriving (Eq, Ord, Read, Show)++-- | Parameter entity reference+newtype ParameterEntityRef = ParameterEntityRef Text+  deriving (Eq, Ord, Read, Show)++-- | @<!ENTITY@+tokenEntityOpen :: CharParsing m => m ()+tokenEntityOpen = void $ string "<!ENTITY"++-- | @<!ELEMENT@+tokenElementTypeOpen :: CharParsing m => m ()+tokenElementTypeOpen = void $ string "<!ELEMENT"++-- | @EMPTY@+tokenElementTypeContentEmpty :: CharParsing m => m ()+tokenElementTypeContentEmpty = void $ string "EMPTY"++-- | @ANY@+tokenElementTypeContentAny :: CharParsing m => m ()+tokenElementTypeContentAny = void $ string "ANY"++-- | @<!ATTLIST@+tokenAttributeListOpen :: CharParsing m => m ()+tokenAttributeListOpen = void $ string "<!ATTLIST"++-- | @%@+tokenPercent :: CharParsing m => m ()+tokenPercent = void $ char '%'++-- | @<!NOTATION@+tokenNotationOpen :: CharParsing m => m ()+tokenNotationOpen = void $ string "<!NOTATION"++-- | @PUBLIC@+tokenPublic :: CharParsing m => m ()+tokenPublic = void $ string "PUBLIC"++-- | <https://www.w3.org/TR/REC-xml/#NT-PEReference>+--+-- >>> parseOnly tokenParameterEntityRef "%foo;"+-- Right (ParameterEntityRef "foo")+tokenParameterEntityRef :: CharParsing m => Monad m => m ParameterEntityRef+tokenParameterEntityRef = ParameterEntityRef <$> (char '%' *> tokenName <* char ';')++-- | <https://www.w3.org/TR/REC-xml/#NT-EntityValue>+tokenEntityValue :: CharParsing m => Monad m => String -> m EntityValue+tokenEntityValue forbiddenChars = (ValueText . Text.pack <$> some (noneOf $ '%':'&':forbiddenChars))+  <|> (ValueParameterEntityRef <$> tokenParameterEntityRef)+  <|> (ValueReference <$> tokenReference)

@@ -0,0 +1,209 @@+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE StandaloneDeriving         #-}+-- | Mid-level parsers for doctype's internal subset, built on top of "Data.XML.InternalSubset.Parser.Low":+--+-- - some formatting details are abstracted away (e.g. quoting, whitespacing), therefore parsers are not reversible+-- - entities delimited by an opening and closing sequence are recognized+-- - token parsers do not overlap, therefore XML document can be tokenized in a stateless way+--+-- All documentation examples assume the following setup:+--+-- > :set -XOverloadedStrings+-- > import Data.Attoparsec.ByteString+module Data.XML.InternalSubset.Parser.Mid+  ( module Data.XML.Parser.Mid.Comment+  , module Data.XML.Parser.Mid.ExternalID+  , module Data.XML.Parser.Mid.Instruction+  , ElementType(..)+  , AttributeList(..)+  , GeneralEntity(..)+  , ParameterEntity(..)+  , Notation(..)+  , Token(..)+  , TokenParser()+  , runTokenParser+  , tokenElementType+  , tokenAttributeList+  , tokenGeneralEntity+  , tokenParameterEntity+  , tokenNotation+  , tokenInstruction+  , tokenComment+  , anyToken+  ) where++import           Control.Applicative+import           Control.Monad.Fail.Compat+import           Data.Functor+import           Data.Text                          (Text)+import qualified Data.Text                          as Text+import           Data.XML.InternalSubset.Parser.Low+import           Data.XML.Parser.Low+import           Data.XML.Parser.Mid.Comment+import           Data.XML.Parser.Mid.ExternalID+import           Data.XML.Parser.Mid.Instruction+import           Text.Parser.Char+import           Text.Parser.Combinators++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> import Data.Attoparsec.ByteString++data Token+  = TokenElementType ElementType+  | TokenAttributeList AttributeList+  | TokenGeneralEntity GeneralEntity+  | TokenParameterEntity ParameterEntity+  | TokenNotation Notation+  | TokenInstruction Instruction+  | TokenComment Text+  deriving (Eq, Ord, Show)++-- | A parser that consumes whole 'Token's.+newtype TokenParser m a = TokenParser { runTokenParser :: m a }++deriving instance Functor m => Functor (TokenParser m)+deriving instance Applicative m => Applicative (TokenParser m)+deriving instance Alternative m => Alternative (TokenParser m)+deriving instance Monad m => Monad (TokenParser m)++instance (Parsing m, Monad m) => MonadFail (TokenParser m) where+  fail = TokenParser . unexpected++-- | <https://www.w3.org/TR/REC-xml/#dt-eldecl>+data ElementType = ElementType Text ElementTypeContent+  deriving (Eq, Ord, Read, Show)++-- | <https://www.w3.org/TR/REC-xml/#NT-elementdecl>+--+-- Missing: mixed | children+data ElementTypeContent = ContentEmpty | ContentAny+  deriving (Eq, Ord, Read, Show)++-- | <https://www.w3.org/TR/REC-xml/#NT-AttlistDecl>+--+-- Missing: attribute definition+newtype AttributeList = AttributeList Text+  deriving (Eq, Ord, Read, Show)++-- | <https://www.w3.org/TR/REC-xml/#gen-entity>+data GeneralEntity = GeneralEntity Text [Content]+  deriving (Eq, Ord, Read, Show)++-- | <https://www.w3.org/TR/REC-xml/#dt-PE>+data ParameterEntity = ParameterEntity Text [EntityValue]+  deriving (Eq, Ord, Read, Show)++-- | <https://www.w3.org/TR/REC-xml/#dt-notation>+data Notation = Notation Text ExternalID+  deriving (Eq, Ord, Read, Show)+++-- | <https://www.w3.org/TR/REC-xml/#NT-contentspec>+elementTypeContent :: CharParsing m => m ElementTypeContent+elementTypeContent = (tokenElementTypeContentEmpty $> ContentEmpty)+  <|> (tokenElementTypeContentAny $> ContentAny)++-- | <https://www.w3.org/TR/REC-xml/#NT-elementdecl>+--+-- >>> parseOnly (runTokenParser tokenElementType) "<!ELEMENT br EMPTY>"+-- Right (ElementType "br" ContentEmpty)+-- >>> parseOnly (runTokenParser tokenElementType) "<!ELEMENT container ANY>"+-- Right (ElementType "container" ContentAny)+tokenElementType :: CharParsing m => Monad m => TokenParser m ElementType+tokenElementType = TokenParser $ do+  tokenElementTypeOpen+  tokenWhitespace+  name <- tokenName+  tokenWhitespace+  content <- elementTypeContent+  optional tokenWhitespace+  tokenElementClose+  pure $ ElementType name content++-- | <https://www.w3.org/TR/REC-xml/#NT-AttlistDecl>+--+-- >>> parseOnly (runTokenParser tokenAttributeList) "<!ATTLIST termdef>"+-- Right (AttributeList "termdef")+tokenAttributeList :: CharParsing m => Monad m => TokenParser m AttributeList+tokenAttributeList = TokenParser $ do+  tokenAttributeListOpen+  tokenWhitespace+  name <- tokenName+  optional tokenWhitespace+  tokenElementClose+  pure $ AttributeList name++-- | <https://www.w3.org/TR/REC-xml/#NT-GEDecl>+--+-- >>> parseOnly (runTokenParser tokenGeneralEntity) "<!ENTITY d '&#xD;'>"+-- Right (GeneralEntity "d" [ContentReference (CharRef '\r')])+-- >>> parseOnly (runTokenParser tokenGeneralEntity) "<!ENTITY da '&#xD;&#xA;'>"+-- Right (GeneralEntity "da" [ContentReference (CharRef '\r'),ContentReference (CharRef '\n')])+-- >>> parseOnly (runTokenParser tokenGeneralEntity) "<!ENTITY Pub-Status 'This is a pre-release of the specification.'>"+-- Right (GeneralEntity "Pub-Status" [ContentText "This is a pre-release of the specification."])+tokenGeneralEntity :: CharParsing m => Monad m => TokenParser m GeneralEntity+tokenGeneralEntity = TokenParser $ do+  tokenEntityOpen+  tokenWhitespace+  name <- tokenName+  tokenWhitespace+  quote <- tokenQuote+  definition <- many (tokenContent $ quote:"%")+  char quote+  optional tokenWhitespace+  tokenElementClose+  return $ GeneralEntity name definition++-- | <https://www.w3.org/TR/REC-xml/#NT-PEDecl>+--+-- >>> parseOnly (runTokenParser tokenParameterEntity) "<!ENTITY % YN '\"Yes\"' >"+-- Right (ParameterEntity "YN" [ValueText "\"Yes\""])+tokenParameterEntity :: CharParsing m => Monad m => TokenParser m ParameterEntity+tokenParameterEntity = TokenParser $ do+  tokenEntityOpen+  tokenWhitespace+  tokenPercent+  tokenWhitespace+  name <- tokenName+  tokenWhitespace+  quote <- tokenQuote+  definition <- many (tokenEntityValue [quote])+  char quote+  optional tokenWhitespace+  tokenElementClose+  pure $ ParameterEntity name definition++-- | <https://www.w3.org/TR/REC-xml/#NT-NotationDecl>+--+-- >>> parseOnly (runTokenParser tokenNotation) "<!NOTATION foo SYSTEM \"identifier\">"+-- Right (Notation "foo" (SystemID "identifier"))+tokenNotation :: CharParsing m => Monad m => TokenParser m Notation+tokenNotation = TokenParser $ do+  tokenNotationOpen+  tokenWhitespace+  name <- tokenName+  tokenWhitespace+  externalEntity <- externalID -- TODO: support PUBLIC ID+  optional tokenWhitespace+  tokenElementClose+  pure $ Notation name externalEntity++-- | <https://www.w3.org/TR/REC-xml/#dt-pi>+tokenInstruction :: CharParsing m => Monad m => TokenParser m Instruction+tokenInstruction = TokenParser instruction++-- | <https://www.w3.org/TR/REC-xml/#NT-Comment>+tokenComment :: CharParsing m => Monad m => TokenParser m Text+tokenComment = TokenParser comment++-- | Parse any 'Token'.+anyToken :: CharParsing m => Monad m => TokenParser m Token+anyToken = TokenElementType <$> tokenElementType+  <|> TokenAttributeList <$> tokenAttributeList+  <|> TokenGeneralEntity <$> tokenGeneralEntity+  <|> TokenParameterEntity <$> tokenParameterEntity+  <|> TokenNotation <$> tokenNotation+  <|> TokenInstruction <$> tokenInstruction+  <|> TokenComment <$> tokenComment

@@ -53,7 +53,7 @@ import           Data.XML.Parser.High.AttrParser import           Data.XML.Parser.High.NameParser import           Data.XML.Parser.Low-import qualified Data.XML.Parser.Mid             as L1+import qualified Data.XML.Parser.Mid             as Mid import           Data.XML.Parser.Mid.Attribute import           Prelude                         () import           Prelude.Compat@@ -68,14 +68,14 @@  -- | XML document prolog. data Prolog = Prolog-  { prologXmlDeclaration :: Maybe L1.XMLDeclaration-  , prologInstructions   :: [L1.Instruction]-  , prologDoctype        :: Maybe L1.Doctype+  { prologXmlDeclaration :: Maybe Mid.XMLDeclaration+  , prologInstructions   :: [Mid.Instruction]+  , prologDoctype        :: Maybe Mid.Doctype   } deriving (Eq, Ord, Read, Show)  data Token   = TokenProlog Prolog-  | TokenInstruction L1.Instruction+  | TokenInstruction Mid.Instruction   | TokenTag QName (Map QName Text) [Token]   | TokenTextContent Text   deriving (Eq, Ord, Read, Show)@@ -143,10 +143,10 @@ -- Right (Instruction "php" "echo 'Hello World!'; ") -- >>> parseOnly (runTokenParser instruction) "<!-- comments and whitespace are ignored -->  <?php echo 'Hello World!'; ?>" -- Right (Instruction "php" "echo 'Hello World!'; ")-instruction :: CharParsing m => Monad m => TokenParser m L1.Instruction+instruction :: CharParsing m => Monad m => TokenParser m Mid.Instruction instruction = TokenParser $ do   skipCommentsWhitespace-  L1.runTokenParser L1.tokenInstruction+  Mid.runTokenParser Mid.tokenInstruction  -- | <https://www.w3.org/TR/REC-xml/#NT-prolog> --@@ -156,12 +156,12 @@ -- Right (Prolog {prologXmlDeclaration = Just (XMLDeclaration "1.0" ...), prologInstructions = [], prologDoctype = Just (Doctype "greeting" ...)}) prolog :: CharParsing m => Monad m => TokenParser m Prolog prolog = TokenParser $ do-  xmlDeclaration <- optional $ L1.runTokenParser L1.tokenXmlDeclaration+  xmlDeclaration <- optional $ Mid.runTokenParser Mid.tokenXmlDeclaration   skipCommentsWhitespace   instructions <- runTokenParser $ many instruction   doctype <- optional $ do     skipCommentsWhitespace-    L1.runTokenParser L1.tokenDoctype+    Mid.runTokenParser Mid.tokenDoctype    when (isNothing xmlDeclaration && null instructions && isNothing doctype)     $ unexpected "Expected XML prolog"@@ -173,8 +173,8 @@ textContent :: CharParsing m => Monad m => EntityDecoder -> TokenParser m Text textContent entityDecoder = TokenParser $ mconcat <$> do   skipComments-  (textualData <|> L1.runTokenParser L1.tokenCdata) `sepBy1` L1.runTokenParser L1.tokenComment-  where textualData = expandContents entityDecoder =<< L1.runTokenParser L1.tokenData+  (textualData <|> Mid.runTokenParser Mid.tokenCdata) `sepBy1` Mid.runTokenParser Mid.tokenComment+  where textualData = expandContents entityDecoder =<< Mid.runTokenParser Mid.tokenData  -- | Same as @textContent (decodePredefinedEntities <> decodeHtmlEntities)@, provided for convenience. --@@ -200,7 +200,7 @@ tag entityDecoder parseName parseAttributes parseContent = parseStartToEnd <|> parseEmptyElement where   parseStartToEnd = TokenParser $ do     skipCommentsWhitespace-    L1.StartTag name attributes <- L1.runTokenParser L1.tokenStartTag+    Mid.StartTag name attributes <- Mid.runTokenParser Mid.tokenStartTag     a <- processName name     b <- processAttributes a attributes     c <- case parseContent b of@@ -208,13 +208,13 @@       AnyContent f       -> f =<< runTokenParser (many $ anyToken entityDecoder)       WithContent parser -> runTokenParser parser     skipCommentsWhitespace-    L1.runTokenParser $ do-      name' <- L1.tokenEndTag+    Mid.runTokenParser $ do+      name' <- Mid.tokenEndTag       when (name /= name') $ fail "Invalid end tag name"     return c   parseEmptyElement = TokenParser $ do     skipCommentsWhitespace-    L1.EmptyElementTag name attributes <- L1.runTokenParser L1.tokenEmptyElementTag+    Mid.EmptyElementTag name attributes <- Mid.runTokenParser Mid.tokenEmptyElementTag     a <- processName name     b <- processAttributes a attributes     case parseContent b of@@ -269,10 +269,10 @@ -- * Private functions  skipComments :: CharParsing m => Monad m => m ()-skipComments = void $ many $ L1.runTokenParser L1.tokenComment+skipComments = void $ many $ Mid.runTokenParser Mid.tokenComment  skipCommentsWhitespace :: CharParsing m => Monad m => m ()-skipCommentsWhitespace = void $ many $ void (L1.runTokenParser L1.tokenComment) <|> void tokenWhitespace+skipCommentsWhitespace = void $ many $ void (Mid.runTokenParser Mid.tokenComment) <|> void tokenWhitespace  decodeStandardEntities :: EntityDecoder decodeStandardEntities = decodePredefinedEntities <> decodeHtmlEntities

@@ -11,18 +11,22 @@ module Data.XML.Parser.Low   ( module Data.XML.Parser.Low.Entity   , module Data.XML.Parser.Low.Name+  , module Data.XML.Parser.Low.Reference   , module Data.XML.Parser.Low+  , module Data.XML.InternalSubset.Parser.Low   ) where  import           Control.Applicative-import           Control.Arrow           ((>>>))+import           Control.Arrow                      ((>>>)) import           Control.Monad import           Data.Char import           Data.Functor-import           Data.Text               (Text)-import qualified Data.Text               as Text+import           Data.Text                          (Text)+import qualified Data.Text                          as Text+import           Data.XML.InternalSubset.Parser.Low import           Data.XML.Parser.Low.Entity import           Data.XML.Parser.Low.Name+import           Data.XML.Parser.Low.Reference import           Numeric import           Text.Parser.Char import           Text.Parser.Combinators@@ -38,26 +42,13 @@  -- | Expand content reference, if any. expandContent :: Alternative m => EntityDecoder -> Content -> m Text-expandContent _ (ContentText t) = pure t+expandContent _ (ContentText t)      = pure t expandContent f (ContentReference r) = expandReference f r  -- | Same as 'expandContent', but on a list. Provided for convenience. expandContents :: Alternative m => Monad m => EntityDecoder -> [Content] -> m Text expandContents f contents = mconcat <$> mapM (expandContent f) contents --- | Entity reference, or character reference.-data Reference = EntityRef Text | CharRef Char-  deriving (Eq, Ord, Read, Show)---- | Resolve reference into raw text.-expandReference :: Alternative m => EntityDecoder -> Reference -> m Text-expandReference _ (CharRef c) = pure $ Text.pack [c]-expandReference f (EntityRef name) = maybe empty pure $ runEntityDecoder f name---- | Same as @expandReference decodePredefinedEntities@, provided for convenience.-expandReference' :: Reference -> Maybe Text-expandReference' = expandReference decodePredefinedEntities- -- | @'@ tokenSingleQuote :: CharParsing m => m Char tokenSingleQuote = char '\''@@ -87,30 +78,9 @@   optional tokenWhitespace   return () --- | <https://www.w3.org/TR/REC-xml/#NT-Reference>------ >>> parseOnly tokenReference "&#x3C;"--- Right (CharRef '<')--- >>> parseOnly tokenReference "&docdate;"--- Right (EntityRef "docdate")-tokenReference :: CharParsing m => Monad m => m Reference-tokenReference = (EntityRef <$> entityRef) <|> (CharRef <$> decCharRef) <|> (CharRef <$> hexCharRef) where-  entityRef = char '&' *> tokenName <* char ';'-  decCharRef = between (string "&#") (char ';') $-    some digit >>= (readDec >>> liftParser "decimal") <&> chr--  hexCharRef = between (string "&#x") (char ';') $-    some hexDigit >>= (readHex >>> liftParser "hexadecimal") <&> chr-  liftParser _ ((result, _):_) = return result-  liftParser message _         = unexpected $ "Failed to parse " <> message- tokenContent :: CharParsing m => Monad m => String -> m Content tokenContent forbiddenChars = (ContentText . Text.pack <$> some (noneOf $ '&':forbiddenChars))   <|> (ContentReference <$> tokenReference)---- | @<!ENTITY@-tokenEntityDeclarationOpen :: CharParsing m => m ()-tokenEntityDeclarationOpen = void $ string "<!ENTITY"  -- | Return processing instruction name. --

@@ -0,0 +1,55 @@+-- | Low-level parsers for XML references.+--+-- All documentation examples assume the following setup:+--+-- > :set -XOverloadedStrings+-- > import Data.Attoparsec.ByteString+module Data.XML.Parser.Low.Reference where++import           Control.Applicative+import           Control.Arrow              ((>>>))+import           Data.Char+import           Data.Functor+import           Data.Text                  (Text)+import qualified Data.Text                  as Text+import           Data.XML.Parser.Low.Entity+import           Data.XML.Parser.Low.Name+import           Numeric+import           Text.Parser.Char+import           Text.Parser.Combinators++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> import Data.Attoparsec.ByteString++-- | <https://www.w3.org/TR/REC-xml/#dt-entref>+--+-- Entity reference, or character reference.+data Reference = EntityRef Text | CharRef Char+  deriving (Eq, Ord, Read, Show)++-- | Resolve reference into raw text.+expandReference :: Alternative m => EntityDecoder -> Reference -> m Text+expandReference _ (CharRef c)      = pure $ Text.pack [c]+expandReference f (EntityRef name) = maybe empty pure $ runEntityDecoder f name++-- | Same as @expandReference decodePredefinedEntities@, provided for convenience.+expandReference' :: Reference -> Maybe Text+expandReference' = expandReference decodePredefinedEntities++-- | <https://www.w3.org/TR/REC-xml/#NT-Reference>+--+-- >>> parseOnly tokenReference "&#x3C;"+-- Right (CharRef '<')+-- >>> parseOnly tokenReference "&docdate;"+-- Right (EntityRef "docdate")+tokenReference :: CharParsing m => Monad m => m Reference+tokenReference = (EntityRef <$> entityRef) <|> (CharRef <$> decCharRef) <|> (CharRef <$> hexCharRef) where+  entityRef = char '&' *> tokenName <* char ';'+  decCharRef = between (string "&#") (char ';') $+    some digit >>= (readDec >>> liftParser "decimal") <&> chr++  hexCharRef = between (string "&#x") (char ';') $+    some hexDigit >>= (readHex >>> liftParser "hexadecimal") <&> chr+  liftParser _ ((result, _):_) = return result+  liftParser message _         = unexpected $ "Failed to parse " <> message

@@ -18,8 +18,9 @@ -- > import Data.Attoparsec.ByteString module Data.XML.Parser.Mid   ( module Data.XML.Parser.Mid.Attribute+  , module Data.XML.Parser.Mid.Comment   , module Data.XML.Parser.Mid.Doctype-  , Instruction(..)+  , module Data.XML.Parser.Mid.Instruction   , XMLDeclaration(..)   , StartTag(..)   , EmptyElementTag(..)@@ -39,17 +40,19 @@   ) where  import           Control.Applicative-import           Control.Arrow                 ((>>>))+import           Control.Arrow                   ((>>>)) import           Control.Monad.Compat import           Control.Monad.Fail.Compat import           Data.Char import           Data.Functor import           Data.Maybe-import           Data.Text                     (Text)-import qualified Data.Text                     as Text+import           Data.Text                       (Text)+import qualified Data.Text                       as Text import           Data.XML.Parser.Low import           Data.XML.Parser.Mid.Attribute+import           Data.XML.Parser.Mid.Comment import           Data.XML.Parser.Mid.Doctype+import           Data.XML.Parser.Mid.Instruction import           Numeric import           Text.Parser.Char import           Text.Parser.Combinators@@ -71,12 +74,6 @@   | TokenCDATA Text   deriving (Eq, Ord, Show) --- | Processing instruction.------ <https://www.w3.org/TR/REC-xml/#dt-pi>-data Instruction = Instruction Text Text-  deriving (Eq, Ord, Read, Show)- -- | <https://www.w3.org/TR/REC-xml/#dt-xmldecl> data XMLDeclaration = XMLDeclaration Text (Maybe Text) (Maybe Bool)   deriving (Eq, Ord, Read, Show)@@ -102,36 +99,16 @@   -- | <https://www.w3.org/TR/REC-xml/#NT-doctypedecl>------ >>> parseOnly (runTokenParser tokenDoctype) "<!DOCTYPE greeting SYSTEM 'hello.dtd'>"--- Right (Doctype "greeting" (Just (SystemID "hello.dtd")) [])--- >>> parseOnly (runTokenParser tokenDoctype) "<!DOCTYPE foo [ <!ENTITY x '&lt;'> ]>"--- Right (Doctype "foo" Nothing [GeneralEntityDeclaration "x" [ContentReference (EntityRef "lt")]]) tokenDoctype :: CharParsing m => Monad m => TokenParser m Doctype tokenDoctype = TokenParser doctype  -- | <https://www.w3.org/TR/REC-xml/#dt-pi>------ >>> parseOnly (runTokenParser tokenInstruction) "<?xml-stylesheet type='text/xsl' href='style.xsl'?>"--- Right (Instruction "xml-stylesheet" "type='text/xsl' href='style.xsl'") tokenInstruction :: CharParsing m => Monad m => TokenParser m Instruction-tokenInstruction = TokenParser $ do-  name <- tokenInstructionOpen-  tokenWhitespace-  content <- manyTill anyChar $ try tokenInstructionClose-  return $ Instruction name $ Text.pack content+tokenInstruction = TokenParser instruction  -- | <https://www.w3.org/TR/REC-xml/#NT-Comment>------ >>> parseOnly (runTokenParser tokenComment) "<!-- declarations for <head> & <body> -->"--- Right " declarations for <head> & <body> "--- >>> parseOnly (runTokenParser tokenComment) "<!-- B+, B, or B--->"--- Right " B+, B, or B-" tokenComment :: CharParsing m => Monad m => TokenParser m Text-tokenComment = TokenParser $ do-  tokenCommentOpen-  content <- manyTill anyChar $ try tokenCommentClose-  return $ Text.pack content+tokenComment = TokenParser comment  -- | <https://www.w3.org/TR/REC-xml/#dt-cdsection> --

@@ -0,0 +1,30 @@+-- | Mid-level parsers for XML comments+--+-- All documentation examples assume the following setup:+--+-- > :set -XOverloadedStrings+-- > import Data.Attoparsec.ByteString+module Data.XML.Parser.Mid.Comment where++import           Control.Monad.Compat+import           Data.Text               (Text)+import qualified Data.Text               as Text+import           Data.XML.Parser.Low+import           Text.Parser.Char+import           Text.Parser.Combinators++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> import Data.Attoparsec.ByteString++-- | <https://www.w3.org/TR/REC-xml/#NT-Comment>+--+-- >>> parseOnly comment "<!-- declarations for <head> & <body> -->"+-- Right " declarations for <head> & <body> "+-- >>> parseOnly comment "<!-- B+, B, or B--->"+-- Right " B+, B, or B-"+comment :: CharParsing m => Monad m => m Text+comment = do+  tokenCommentOpen+  content <- manyTill anyChar $ try tokenCommentClose+  return $ Text.pack content

@@ -7,19 +7,17 @@ -- > :set -XOverloadedStrings -- > import Data.Attoparsec.ByteString module Data.XML.Parser.Mid.Doctype-  ( ExternalID(..)-  , externalID-  , GeneralEntityDeclaration(..)-  , generalEntityDeclaration-  , Doctype(..)+  ( Doctype(..)   , doctype   ) where -import Control.Applicative-import Data.Maybe-import qualified Data.Text as Text-import Data.Text (Text)+import           Control.Applicative+import           Data.Maybe+import           Data.Text                           (Text)+import qualified Data.Text                           as Text+import           Data.XML.InternalSubset.Parser.High import           Data.XML.Parser.Low+import           Data.XML.Parser.Mid.ExternalID import           Text.Parser.Char import           Text.Parser.Combinators @@ -27,66 +25,17 @@ -- >>> :set -XOverloadedStrings -- >>> import Data.Attoparsec.ByteString --- | External entity identifier------ <https://www.w3.org/TR/REC-xml/#dt-extent>-data ExternalID = PublicID Text Text | SystemID Text-  deriving (Eq, Ord, Read, Show)---- | <https://www.w3.org/TR/REC-xml/#gen-entity>-data GeneralEntityDeclaration = GeneralEntityDeclaration Text [Content]-  deriving (Eq, Ord, Read, Show)- -- | <https://www.w3.org/TR/REC-xml/#dt-doctype>-data Doctype = Doctype Text (Maybe ExternalID) [GeneralEntityDeclaration]+data Doctype = Doctype Text (Maybe ExternalID) InternalSubset   deriving (Eq, Ord, Read, Show)  --- | <https://www.w3.org/TR/REC-xml/#NT-GEDecl>------ >>> parseOnly generalEntityDeclaration "<!ENTITY d '&#xD;'>"--- Right (GeneralEntityDeclaration "d" [ContentReference (CharRef '\r')])--- >>> parseOnly generalEntityDeclaration "<!ENTITY da '&#xD;&#xA;'>"--- Right (GeneralEntityDeclaration "da" [ContentReference (CharRef '\r'),ContentReference (CharRef '\n')])--- >>> parseOnly generalEntityDeclaration "<!ENTITY Pub-Status 'This is a pre-release of the specification.'>"--- Right (GeneralEntityDeclaration "Pub-Status" [ContentText "This is a pre-release of the specification."])-generalEntityDeclaration :: CharParsing m => Monad m => m GeneralEntityDeclaration-generalEntityDeclaration = do-  tokenEntityDeclarationOpen-  tokenWhitespace-  name <- tokenName-  tokenWhitespace-  quote <- tokenQuote-  definition <- many (tokenContent $ quote:"%")-  char quote-  optional tokenWhitespace-  tokenElementClose-  return $ GeneralEntityDeclaration name definition---- | <https://www.w3.org/TR/REC-xml/#NT-ExternalID>------ >>> parseOnly externalID "PUBLIC '-//Textuality//TEXT Standard open-hatch boilerplate//EN' 'http://www.textuality.com/boilerplate/OpenHatch.xml'"--- Right (PublicID "-//Textuality//TEXT Standard open-hatch boilerplate//EN" "http://www.textuality.com/boilerplate/OpenHatch.xml")--- >>> parseOnly externalID "SYSTEM '../grafix/OpenHatch.gif'"--- Right (SystemID "../grafix/OpenHatch.gif")-externalID :: CharParsing m => Monad m => m ExternalID-externalID = publicID <|> systemID where-  publicID = do-    string "PUBLIC"-    tokenWhitespace-    a <- systemLiteral-    tokenWhitespace-    b <- systemLiteral-    return $ PublicID a b-  systemID = string "SYSTEM" *> tokenWhitespace *> (SystemID <$> systemLiteral)-  systemLiteral = Text.pack <$> manyQuoted anyChar- -- | <https://www.w3.org/TR/REC-xml/#NT-doctypedecl> -- -- >>> parseOnly doctype "<!DOCTYPE greeting SYSTEM 'hello.dtd'>"--- Right (Doctype "greeting" (Just (SystemID "hello.dtd")) [])+-- Right (Doctype "greeting" (Just (SystemID "hello.dtd")) (InternalSubset {_elementTypes = [], _attributeLists = [], _generalEntities = [], _parameterEntities = [], _notations = [], _instructions = []})) -- >>> parseOnly doctype "<!DOCTYPE foo [ <!ENTITY x '&lt;'> ]>"--- Right (Doctype "foo" Nothing [GeneralEntityDeclaration "x" [ContentReference (EntityRef "lt")]])+-- Right (Doctype "foo" Nothing (InternalSubset {_elementTypes = [], _attributeLists = [], _generalEntities = [GeneralEntity "x" [ContentReference (EntityRef "lt")]], _parameterEntities = [], _notations = [], _instructions = []})) doctype :: CharParsing m => Monad m => m Doctype doctype = do   tokenDoctypeOpen@@ -94,18 +43,8 @@   name <- tokenName   externalID <- optional $ tokenWhitespace >> externalID   optional tokenWhitespace-  entities <- fromMaybe mempty <$> optional-    (between (char '[' >> optional tokenWhitespace) (optional tokenWhitespace >> char ']') $-      many generalEntityDeclaration)+  entities <- fromMaybe emptyInternalSubset <$> optional+    (between (char '[' >> optional tokenWhitespace) (optional tokenWhitespace >> char ']')+      internalSubset)   tokenElementClose   return $ Doctype name externalID entities---quoted :: CharParsing m => Monad m => m a -> m a-quoted x = x `surroundedBy` tokenSingleQuote <|> x `surroundedBy` tokenDoubleQuote--manyQuoted :: CharParsing m => Monad m => m a -> m [a]-manyQuoted x = manyQuotedBy tokenSingleQuote x <|> manyQuotedBy tokenDoubleQuote x where-  manyQuotedBy quote x = do-    quote-    manyTill x (try quote)

@@ -0,0 +1,58 @@+-- | Mid-level parsers for XML external entities.+--+-- <https://www.w3.org/TR/REC-xml/#dt-extent>+--+-- All documentation examples assume the following setup:+--+-- > :set -XOverloadedStrings+-- > import Data.Attoparsec.ByteString+module Data.XML.Parser.Mid.ExternalID+  ( ExternalID(..)+  , externalID+  ) where++import           Control.Applicative+import           Data.Text               (Text)+import qualified Data.Text               as Text+import           Data.XML.Parser.Low+import           Text.Parser.Char+import           Text.Parser.Combinators++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> import Data.Attoparsec.ByteString+++-- | External entity identifier+--+-- <https://www.w3.org/TR/REC-xml/#dt-extent>+data ExternalID = PublicID Text Text | SystemID Text+  deriving (Eq, Ord, Read, Show)+++-- | <https://www.w3.org/TR/REC-xml/#NT-ExternalID>+--+-- >>> parseOnly externalID "PUBLIC '-//Textuality//TEXT Standard open-hatch boilerplate//EN' 'http://www.textuality.com/boilerplate/OpenHatch.xml'"+-- Right (PublicID "-//Textuality//TEXT Standard open-hatch boilerplate//EN" "http://www.textuality.com/boilerplate/OpenHatch.xml")+-- >>> parseOnly externalID "SYSTEM '../grafix/OpenHatch.gif'"+-- Right (SystemID "../grafix/OpenHatch.gif")+externalID :: CharParsing m => Monad m => m ExternalID+externalID = publicID <|> systemID where+  publicID = do+    string "PUBLIC"+    tokenWhitespace+    a <- systemLiteral+    tokenWhitespace+    b <- systemLiteral+    return $ PublicID a b+  systemID = string "SYSTEM" *> tokenWhitespace *> (SystemID <$> systemLiteral)+  systemLiteral = Text.pack <$> manyQuoted anyChar++quoted :: CharParsing m => Monad m => m a -> m a+quoted x = x `surroundedBy` tokenSingleQuote <|> x `surroundedBy` tokenDoubleQuote++manyQuoted :: CharParsing m => Monad m => m a -> m [a]+manyQuoted x = manyQuotedBy tokenSingleQuote x <|> manyQuotedBy tokenDoubleQuote x where+  manyQuotedBy quote x = do+    quote+    manyTill x (try quote)

@@ -0,0 +1,35 @@+-- | Mid-level parsers for XML instructions.+--+-- All documentation examples assume the following setup:+--+-- > :set -XOverloadedStrings+-- > import Data.Attoparsec.ByteString+module Data.XML.Parser.Mid.Instruction where++import           Data.Text               (Text)+import qualified Data.Text               as Text+import           Data.XML.Parser.Low+import           Text.Parser.Char+import           Text.Parser.Combinators++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> import Data.Attoparsec.ByteString++-- | Processing instruction.+--+-- <https://www.w3.org/TR/REC-xml/#dt-pi>+data Instruction = Instruction Text Text+  deriving (Eq, Ord, Read, Show)+++-- | <https://www.w3.org/TR/REC-xml/#dt-pi>+--+-- >>> parseOnly instruction "<?xml-stylesheet type='text/xsl' href='style.xsl'?>"+-- Right (Instruction "xml-stylesheet" "type='text/xsl' href='style.xsl'")+instruction :: CharParsing m => Monad m => m Instruction+instruction = do+  name <- tokenInstructionOpen+  tokenWhitespace+  content <- manyTill anyChar $ try tokenInstructionClose+  return $ Instruction name $ Text.pack content

@@ -2,7 +2,9 @@     [ TokenProlog         ( Prolog             { prologXmlDeclaration = Just-                ( XMLDeclaration "1.0" ( Just "utf-8" ) Nothing )+                ( XMLDeclaration "1.0"+                    ( Just "utf-8" ) Nothing+                )             , prologInstructions = []             , prologDoctype = Nothing             }@@ -38,7 +40,8 @@                     , "text"                     )                 ]-            ) [ TokenTextContent "<em>Example</em> Feed" ]+            )+            [ TokenTextContent "<em>Example</em> Feed" ]         , TokenTag             ( QName                 { namePrefix = ""@@ -60,40 +63,50 @@                 { namePrefix = ""                 , nameLocal = "updated"                 }-            ) ( fromList [] ) [ TokenTextContent "2003-12-13T18:30:02Z" ]+            )+            ( fromList [] )+            [ TokenTextContent "2003-12-13T18:30:02Z" ]         , TokenTag             ( QName                 { namePrefix = ""                 , nameLocal = "author"                 }-            ) ( fromList [] )+            )+            ( fromList [] )             [ TokenTag                 ( QName                     { namePrefix = ""                     , nameLocal = "name"                     }-                ) ( fromList [] ) [ TokenTextContent "John Doe" ]+                )+                ( fromList [] )+                [ TokenTextContent "John Doe" ]             , TokenTextContent "-        "+                "             ]         , TokenTag             ( QName                 { namePrefix = ""                 , nameLocal = "id"                 }-            ) ( fromList [] ) [ TokenTextContent "urn:uuid:60a76c80-d399-11d9-b93C-0003939e0af6" ]+            )+            ( fromList [] )+            [ TokenTextContent "urn:uuid:60a76c80-d399-11d9-b93C-0003939e0af6" ]         , TokenTag             ( QName                 { namePrefix = ""                 , nameLocal = "entry"                 }-            ) ( fromList [] )+            )+            ( fromList [] )             [ TokenTag                 ( QName                     { namePrefix = ""                     , nameLocal = "title"                     }-                ) ( fromList [] ) [ TokenTextContent "Atom-Powered Robots Run Amok" ]+                )+                ( fromList [] )+                [ TokenTextContent "Atom-Powered Robots Run Amok" ]             , TokenTag                 ( QName                     { namePrefix = ""@@ -115,23 +128,31 @@                     { namePrefix = ""                     , nameLocal = "id"                     }-                ) ( fromList [] ) [ TokenTextContent "urn:uuid:1225c695-cfb8-4ebb-aaaa-80da344efa6a" ]+                )+                ( fromList [] )+                [ TokenTextContent "urn:uuid:1225c695-cfb8-4ebb-aaaa-80da344efa6a" ]             , TokenTag                 ( QName                     { namePrefix = ""                     , nameLocal = "updated"                     }-                ) ( fromList [] ) [ TokenTextContent "2003-12-13T18:30:02Z" ]+                )+                ( fromList [] )+                [ TokenTextContent "2003-12-13T18:30:02Z" ]             , TokenTag                 ( QName                     { namePrefix = ""                     , nameLocal = "summary"                     }-                ) ( fromList [] ) [ TokenTextContent "Some text." ]+                )+                ( fromList [] )+                [ TokenTextContent "Some text." ]             , TokenTextContent "-        "+                "             ]-        , TokenTextContent ""+        , TokenTextContent "+          "         ]-    , TokenTextContent ""+    , TokenTextContent "+      "     ]

@@ -1,7 +1,11 @@ Right     [ TokenXMLDeclaration-        ( XMLDeclaration "1.0" ( Just "utf-8" ) Nothing )-    , TokenData [ ContentText "" ]+        ( XMLDeclaration "1.0"+            ( Just "utf-8" ) Nothing+        )+    , TokenData+        [ ContentText "+        " ]     , TokenStartTag         ( StartTag             ( QName@@ -14,11 +18,13 @@                     { namePrefix = ""                     , nameLocal = "xmlns"                     }-                ) [ ContentText "http://www.w3.org/2005/Atom" ]+                )+                [ ContentText "http://www.w3.org/2005/Atom" ]             ]         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenStartTag         ( StartTag             ( QName@@ -31,17 +37,22 @@                     { namePrefix = ""                     , nameLocal = "type"                     }-                ) [ ContentText "text" ]+                )+                [ ContentText "text" ]             ]         )     , TokenData-        [ ContentReference ( EntityRef "lt" )+        [ ContentReference+            ( EntityRef "lt" )         , ContentText "em"-        , ContentReference ( EntityRef "gt" )+        , ContentReference+            ( EntityRef "gt" )         , ContentText "Example"-        , ContentReference ( EntityRef "lt" )+        , ContentReference+            ( EntityRef "lt" )         , ContentText "/em"-        , ContentReference ( EntityRef "gt" )+        , ContentReference+            ( EntityRef "gt" )         , ContentText " Feed"         ]     , TokenEndTag@@ -50,8 +61,9 @@             , nameLocal = "title"             }         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenEmptyElementTag         ( EmptyElementTag             ( QName@@ -64,11 +76,13 @@                     { namePrefix = ""                     , nameLocal = "href"                     }-                ) [ ContentText "http://example.org/" ]+                )+                [ ContentText "http://example.org/" ]             ]         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenStartTag         ( StartTag             ( QName@@ -77,15 +91,17 @@                 }             ) []         )-    , TokenData [ ContentText "2003-12-13T18:30:02Z" ]+    , TokenData+        [ ContentText "2003-12-13T18:30:02Z" ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "updated"             }         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenStartTag         ( StartTag             ( QName@@ -94,8 +110,9 @@                 }             ) []         )-    , TokenData [ ContentText "-          " ]+    , TokenData+        [ ContentText "+            " ]     , TokenStartTag         ( StartTag             ( QName@@ -104,23 +121,26 @@                 }             ) []         )-    , TokenData [ ContentText "John Doe" ]+    , TokenData+        [ ContentText "John Doe" ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "name"             }         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "author"             }         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenStartTag         ( StartTag             ( QName@@ -129,15 +149,17 @@                 }             ) []         )-    , TokenData [ ContentText "urn:uuid:60a76c80-d399-11d9-b93C-0003939e0af6" ]+    , TokenData+        [ ContentText "urn:uuid:60a76c80-d399-11d9-b93C-0003939e0af6" ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "id"             }         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenStartTag         ( StartTag             ( QName@@ -146,8 +168,9 @@                 }             ) []         )-    , TokenData [ ContentText "-          " ]+    , TokenData+        [ ContentText "+            " ]     , TokenStartTag         ( StartTag             ( QName@@ -156,15 +179,17 @@                 }             ) []         )-    , TokenData [ ContentText "Atom-Powered Robots Run Amok" ]+    , TokenData+        [ ContentText "Atom-Powered Robots Run Amok" ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "title"             }         )-    , TokenData [ ContentText "-          " ]+    , TokenData+        [ ContentText "+            " ]     , TokenEmptyElementTag         ( EmptyElementTag             ( QName@@ -177,11 +202,13 @@                     { namePrefix = ""                     , nameLocal = "href"                     }-                ) [ ContentText "http://example.org/2003/12/13/atom03" ]+                )+                [ ContentText "http://example.org/2003/12/13/atom03" ]             ]         )-    , TokenData [ ContentText "-          " ]+    , TokenData+        [ ContentText "+            " ]     , TokenStartTag         ( StartTag             ( QName@@ -190,15 +217,17 @@                 }             ) []         )-    , TokenData [ ContentText "urn:uuid:1225c695-cfb8-4ebb-aaaa-80da344efa6a" ]+    , TokenData+        [ ContentText "urn:uuid:1225c695-cfb8-4ebb-aaaa-80da344efa6a" ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "id"             }         )-    , TokenData [ ContentText "-          " ]+    , TokenData+        [ ContentText "+            " ]     , TokenStartTag         ( StartTag             ( QName@@ -207,15 +236,17 @@                 }             ) []         )-    , TokenData [ ContentText "2003-12-13T18:30:02Z" ]+    , TokenData+        [ ContentText "2003-12-13T18:30:02Z" ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "updated"             }         )-    , TokenData [ ContentText "-          " ]+    , TokenData+        [ ContentText "+            " ]     , TokenStartTag         ( StartTag             ( QName@@ -224,27 +255,33 @@                 }             ) []         )-    , TokenData [ ContentText "Some text." ]+    , TokenData+        [ ContentText "Some text." ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "summary"             }         )-    , TokenData [ ContentText "-        " ]+    , TokenData+        [ ContentText "+          " ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "entry"             }         )-    , TokenData [ ContentText "" ]+    , TokenData+        [ ContentText "+        " ]     , TokenEndTag         ( QName             { namePrefix = ""             , nameLocal = "feed"             }         )-    , TokenData [ ContentText "" ]+    , TokenData+        [ ContentText "+        " ]     ]

@@ -0,0 +1,132 @@+<!DOCTYPE html>+<html lang="en">+<head>+        <title>Idris: A Language for Type-Driven Development</title>+        <meta charset="utf-8" />+        <link rel="stylesheet" href="https://www.idris-lang.org/theme/css/main.css" type="text/css" />+        <link href="https://www.idris-lang.org/" type="application/atom+xml" rel="alternate" title="Idris ATOM Feed" />+++        <!--[if IE]>+                <script src="http://html5shiv.googlecode.com/svn/trunk/html5.js"></script><![endif]-->++        <!--[if lte IE 7]>+                <link rel="stylesheet" type="text/css" media="all" href="https://www.idris-lang.org/css/ie.css"/>+                <script src="https://www.idris-lang.org/js/IE8.js" type="text/javascript"></script><![endif]-->++        <!--[if lt IE 7]>+                <link rel="stylesheet" type="text/css" media="all" href="https://www.idris-lang.org/css/ie6.css"/><![endif]-->++</head>++<body id="index" class="home">+        <header id="banner" class="body">+                <h1><a href="https://www.idris-lang.org/index.html">+                        <!--<img src = "https://www.idris-lang.org/images/logo-small.png" alt = "[Idris]" aligh=left>-->+</a></h1>+                <nav><ul>+                <li><a href="https://www.idris-lang.org/index.html">Home</a></li>+                    <li ><a href="https://www.idris-lang.org/pages/download.html">Download</a></li>+                    <li ><a href="https://www.idris-lang.org/pages/example.html">Example</a></li>+                    <li ><a href="https://www.idris-lang.org/pages/documentation.html">Documentation</a></li>+                <!-- <li><a href="https://www.idris-lang.org/">Archives</a></li> -->+                    <li ><a href="https://www.idris-lang.org/category/news.html">News</a></li>+                </ul></nav>+        </header><!-- /#banner -->+++<section id="content" class="body">+    <h1 class="entry-title">Idris: A Language for Type-Driven Development</h1>+    <!-- .. image:: images/profile.jpeg -->+<!-- :alt: [Shape Sorter Box] -->+<!-- :align: right -->+<p>Idris is a programming language designed to encourage <em>Type-Driven+Development</em>.</p>+<p>In type-driven development, types are tools for constructing programs.  We+treat the type as the <em>plan</em> for a program, and use the compiler and type+checker as our assistant, guiding us to a complete program that satisfies the+type. The more expressive the type is that we give up front, the more+confidence we can have that the resulting program will be correct.</p>+<p>In Idris, types are first-class constructs in the langauge. This means types+can be passed as arguments to functions, and returned from functions just like+any other value, such as numbers, strings, or lists. This is a small but+powerful idea, enabling:</p>+<ul class="simple">+<li>relationships to be expressed between values; for example, that two lists+have the same length.</li>+<li>assumptions to be made explicit and checked by the compiler. For example, if+you assume that a list is non-empty, Idris can ensure this assumption always+holds before the program is run.</li>+<li>if desired, properties of program behaviour to be formally stated and+proven.</li>+</ul>+<div class="section" id="getting-started">+<h2>Getting Started</h2>+<p>You can see some <a class="reference external" href="https://www.idris-lang.org/pages/example.html">small examples</a>, then take a+look at the <a class="reference external" href="https://www.idris-lang.org/pages/documentation.html">documentation</a>.</p>+</div>+<div class="section" id="community">+<h2>Community</h2>+<dl class="docutils">+<dt><strong>Mailing list</strong></dt>+<dd>Long-form discussion happens on the <a class="reference external" href="https://groups.google.com/forum/#!forum/idris-lang">mailing list</a>.</dd>+<dt><strong>IRC</strong></dt>+<dd>There is also an irc channel <tt class="docutils literal">#idris</tt> on <a class="reference external" href="irc://chat.freenode.net/idris">freenode</a>.+Point your irc client to <tt class="docutils literal">chat.freenode.net</tt> then <tt class="docutils literal">/join #idris</tt>.+Alternatively, there is a <a class="reference external" href="http://webchat.freenode.net/">web interface</a>.</dd>+<dt><strong>GitHub</strong></dt>+<dd>The Idris source is available from our repository.+Tools and code by the wider Idris community are available in a+<a class="reference external" href="https://github.com/idris-hackers">GitHub organisation</a>.</dd>+<dt><strong>Slack</strong></dt>+<dd>There is an active <tt class="docutils literal">#idris</tt> channel on the+<a class="reference external" href="https://functionalprogramming.slack.com/">Functional Programming</a> Slack.</dd>+</dl>+<p>All participants in these forums are requested to abide by the+<a class="reference external" href="https://www.idris-lang.org/pages/community-standards.html">community standards</a>.</p>+<p>Idris development is led by <a class="reference external" href="http://www.type-driven.org.uk/edwinb/">Edwin Brady</a>+at the <a class="reference external" href="http://www.cs.st-andrews.ac.uk">School of Computer Science, University of St Andrews</a>.</p>+<p>Many thanks to Heath Johns for designing the logo.</p>+</div>+<div class="section" id="support">+<h2>Support</h2>+<p>Idris has been generously supported by the following <a class="reference external" href="https://epsrc.ukri.org/">EPSRC</a> grants:</p>+<ul class="simple">+<li><a class="reference external" href="https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/N024222/1">Type-driven Verification of Communicating Systems</a></li>+<li><a class="reference external" href="https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/T007265/1">Programming as Conversation: Type-Driven Development in Action</a></li>+</ul>+<p>We are also grateful for the continuing support+of <a class="reference external" href="http://www.sicsa.ac.uk/">SICSA</a>, the Scottish Informatics and Computer Science Alliance</p>+</div>++</section>++        <aside id="sidebar">+                <div class="widget">+                        <h2>Categories</h2>+                        <ul>+                           <li ><a href="https://www.idris-lang.org/category/news.html">News</a></li>+                        </ul>+                </div>+                <div class="widget social">+                        <h2>Social</h2>+                        <ul>+                            <li><a href="https://www.idris-lang.org/feeds/all.atom.xml" rel="alternate">atom feed</a></li>++                            <li><a href="https://www.twitter.com/idrislang">@idrislang</a></li>+                            <li><a href="https://www.github.com/idris-lang">GitHub</a></li>+                        </ul>+                </div><!-- /.social -->+        </aside><!-- /#sidebar -->++        <footer id="footer" class="body">+                <address id="about" class="vcard body">+                Proudly powered by <a href="http://alexis.notmyidea.org/pelican/">Pelican</a>, which takes great advantage of <a href="http://python.org">Python</a> (not Idris :)).+                Patches are welcome on <a href="https://github.com/edwinb/idris-lang.org/">github</a>!+                </address><!-- /#about -->++                <p>The theme is «notmyidea-cms», a modified version of «notmyidea», the default theme.</p>+        </footer><!-- /#footer -->++</body>+</html>

@@ -0,0 +1,1570 @@+Right+    [ TokenProlog+        ( Prolog+            { prologXmlDeclaration = Nothing+            , prologInstructions = []+            , prologDoctype = Just+                ( Doctype "html" Nothing+                    ( InternalSubset+                        { _elementTypes = []+                        , _attributeLists = []+                        , _generalEntities = []+                        , _parameterEntities = []+                        , _notations = []+                        , _instructions = []+                        }+                    )+                )+            }+        )+    , TokenTag+        ( QName+            { namePrefix = ""+            , nameLocal = "html"+            }+        )+        ( fromList+            [+                ( QName+                    { namePrefix = ""+                    , nameLocal = "lang"+                    }+                , "en"+                )+            ]+        )+        [ TokenTag+            ( QName+                { namePrefix = ""+                , nameLocal = "head"+                }+            )+            ( fromList [] )+            [ TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "title"+                    }+                )+                ( fromList [] )+                [ TokenTextContent "Idris: A Language for Type-Driven Development" ]+            , TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "meta"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "charset"+                            }+                        , "utf-8"+                        )+                    ]+                ) []+            , TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "link"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "href"+                            }+                        , "https://www.idris-lang.org/theme/css/main.css"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "rel"+                            }+                        , "stylesheet"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "type"+                            }+                        , "text/css"+                        )+                    ]+                ) []+            , TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "link"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "href"+                            }+                        , "https://www.idris-lang.org/"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "rel"+                            }+                        , "alternate"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "title"+                            }+                        , "Idris ATOM Feed"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "type"+                            }+                        , "application/atom+xml"+                        )+                    ]+                ) []+            , TokenTextContent "+++                      ++                      ++                      ++              "+            ]+        , TokenTag+            ( QName+                { namePrefix = ""+                , nameLocal = "body"+                }+            )+            ( fromList+                [+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "class"+                        }+                    , "home"+                    )+                ,+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "id"+                        }+                    , "index"+                    )+                ]+            )+            [ TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "header"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "class"+                            }+                        , "body"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "id"+                            }+                        , "banner"+                        )+                    ]+                )+                [ TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "h1"+                        }+                    )+                    ( fromList [] )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "a"+                            }+                        )+                        ( fromList+                            [+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "href"+                                    }+                                , "https://www.idris-lang.org/index.html"+                                )+                            ]+                        )+                        [ TokenTextContent "+                                                +                        " ]+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "nav"+                        }+                    )+                    ( fromList [] )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "ul"+                            }+                        )+                        ( fromList [] )+                        [ TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/index.html"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Home" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/pages/download.html"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Download" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/pages/example.html"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Example" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/pages/documentation.html"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Documentation" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/category/news.html"+                                        )+                                    ]+                                )+                                [ TokenTextContent "News" ]+                            ]+                        , TokenTextContent "+                                          "+                        ]+                    ]+                , TokenTextContent "+                          "+                ]+            , TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "section"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "class"+                            }+                        , "body"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "id"+                            }+                        , "content"+                        )+                    ]+                )+                [ TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "h1"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "entry-title"+                            )+                        ]+                    )+                    [ TokenTextContent "Idris: A Language for Type-Driven Development" ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "p"+                        }+                    )+                    ( fromList [] )+                    [ TokenTextContent "Idris is a programming language designed to encourage "+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "em"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Type-Driven+                        Development" ]+                    , TokenTextContent "."+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "p"+                        }+                    )+                    ( fromList [] )+                    [ TokenTextContent "In type-driven development, types are tools for constructing programs.  We+                      treat the type as the "+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "em"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "plan" ]+                    , TokenTextContent " for a program, and use the compiler and type+                      checker as our assistant, guiding us to a complete program that satisfies the+                      type. The more expressive the type is that we give up front, the more+                      confidence we can have that the resulting program will be correct."+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "p"+                        }+                    )+                    ( fromList [] )+                    [ TokenTextContent "In Idris, types are first-class constructs in the langauge. This means types+                    can be passed as arguments to functions, and returned from functions just like+                    any other value, such as numbers, strings, or lists. This is a small but+                    powerful idea, enabling:" ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "ul"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "simple"+                            )+                        ]+                    )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "li"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "relationships to be expressed between values; for example, that two lists+                        have the same length." ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "li"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "assumptions to be made explicit and checked by the compiler. For example, if+                        you assume that a list is non-empty, Idris can ensure this assumption always+                        holds before the program is run." ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "li"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "if desired, properties of program behaviour to be formally stated and+                        proven." ]+                    , TokenTextContent "+                      "+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "div"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "section"+                            )+                        ,+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "id"+                                }+                            , "getting-started"+                            )+                        ]+                    )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "h2"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Getting Started" ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "p"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "You can see some "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "https://www.idris-lang.org/pages/example.html"+                                    )+                                ]+                            )+                            [ TokenTextContent "small examples" ]+                        , TokenTextContent ", then take a+                          look at the "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "https://www.idris-lang.org/pages/documentation.html"+                                    )+                                ]+                            )+                            [ TokenTextContent "documentation" ]+                        , TokenTextContent "."+                        ]+                    , TokenTextContent "+                      "+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "div"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "section"+                            )+                        ,+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "id"+                                }+                            , "community"+                            )+                        ]+                    )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "h2"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Community" ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "dl"+                            }+                        )+                        ( fromList+                            [+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "class"+                                    }+                                , "docutils"+                                )+                            ]+                        )+                        [ TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dt"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "strong"+                                    }+                                )+                                ( fromList [] )+                                [ TokenTextContent "Mailing list" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dd"+                                }+                            )+                            ( fromList [] )+                            [ TokenTextContent "Long-form discussion happens on the "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://groups.google.com/forum/#!forum/idris-lang"+                                        )+                                    ]+                                )+                                [ TokenTextContent "mailing list" ]+                            , TokenTextContent "."+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dt"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "strong"+                                    }+                                )+                                ( fromList [] )+                                [ TokenTextContent "IRC" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dd"+                                }+                            )+                            ( fromList [] )+                            [ TokenTextContent "There is also an irc channel "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "tt"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "docutils literal"+                                        )+                                    ]+                                )+                                [ TokenTextContent "#idris" ]+                            , TokenTextContent " on "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "irc://chat.freenode.net/idris"+                                        )+                                    ]+                                )+                                [ TokenTextContent "freenode" ]+                            , TokenTextContent ".+                              Point your irc client to "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "tt"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "docutils literal"+                                        )+                                    ]+                                )+                                [ TokenTextContent "chat.freenode.net" ]+                            , TokenTextContent " then "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "tt"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "docutils literal"+                                        )+                                    ]+                                )+                                [ TokenTextContent "/join #idris" ]+                            , TokenTextContent ".+                              Alternatively, there is a "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "http://webchat.freenode.net/"+                                        )+                                    ]+                                )+                                [ TokenTextContent "web interface" ]+                            , TokenTextContent "."+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dt"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "strong"+                                    }+                                )+                                ( fromList [] )+                                [ TokenTextContent "GitHub" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dd"+                                }+                            )+                            ( fromList [] )+                            [ TokenTextContent "The Idris source is available from our repository.+                              Tools and code by the wider Idris community are available in a+                              "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://github.com/idris-hackers"+                                        )+                                    ]+                                )+                                [ TokenTextContent "GitHub organisation" ]+                            , TokenTextContent "."+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dt"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "strong"+                                    }+                                )+                                ( fromList [] )+                                [ TokenTextContent "Slack" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "dd"+                                }+                            )+                            ( fromList [] )+                            [ TokenTextContent "There is an active "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "tt"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "docutils literal"+                                        )+                                    ]+                                )+                                [ TokenTextContent "#idris" ]+                            , TokenTextContent " channel on the+                              "+                            , TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://functionalprogramming.slack.com/"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Functional Programming" ]+                            , TokenTextContent " Slack."+                            ]+                        , TokenTextContent "+                          "+                        ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "p"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "All participants in these forums are requested to abide by the+                          "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "https://www.idris-lang.org/pages/community-standards.html"+                                    )+                                ]+                            )+                            [ TokenTextContent "community standards" ]+                        , TokenTextContent "."+                        ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "p"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Idris development is led by "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "http://www.type-driven.org.uk/edwinb/"+                                    )+                                ]+                            )+                            [ TokenTextContent "Edwin Brady" ]+                        , TokenTextContent "+                          at the "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "http://www.cs.st-andrews.ac.uk"+                                    )+                                ]+                            )+                            [ TokenTextContent "School of Computer Science, University of St Andrews" ]+                        , TokenTextContent "."+                        ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "p"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Many thanks to Heath Johns for designing the logo." ]+                    , TokenTextContent "+                      "+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "div"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "section"+                            )+                        ,+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "id"+                                }+                            , "support"+                            )+                        ]+                    )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "h2"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Support" ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "p"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Idris has been generously supported by the following "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "https://epsrc.ukri.org/"+                                    )+                                ]+                            )+                            [ TokenTextContent "EPSRC" ]+                        , TokenTextContent " grants:"+                        ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "ul"+                            }+                        )+                        ( fromList+                            [+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "class"+                                    }+                                , "simple"+                                )+                            ]+                        )+                        [ TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/N024222/1"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Type-driven Verification of Communicating Systems" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "class"+                                            }+                                        , "reference external"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/T007265/1"+                                        )+                                    ]+                                )+                                [ TokenTextContent "Programming as Conversation: Type-Driven Development in Action" ]+                            ]+                        , TokenTextContent "+                          "+                        ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "p"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "We are also grateful for the continuing support+                          of "+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "a"+                                }+                            )+                            ( fromList+                                [+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "class"+                                        }+                                    , "reference external"+                                    )+                                ,+                                    ( QName+                                        { namePrefix = ""+                                        , nameLocal = "href"+                                        }+                                    , "http://www.sicsa.ac.uk/"+                                    )+                                ]+                            )+                            [ TokenTextContent "SICSA" ]+                        , TokenTextContent ", the Scottish Informatics and Computer Science Alliance"+                        ]+                    , TokenTextContent "+                      "+                    ]+                , TokenTextContent "++                  "+                ]+            , TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "aside"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "id"+                            }+                        , "sidebar"+                        )+                    ]+                )+                [ TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "div"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "widget"+                            )+                        ]+                    )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "h2"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Categories" ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "ul"+                            }+                        )+                        ( fromList [] )+                        [ TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/category/news.html"+                                        )+                                    ]+                                )+                                [ TokenTextContent "News" ]+                            ]+                        , TokenTextContent "+                                                  "+                        ]+                    , TokenTextContent "+                                      "+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "div"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "widget social"+                            )+                        ]+                    )+                    [ TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "h2"+                            }+                        )+                        ( fromList [] )+                        [ TokenTextContent "Social" ]+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "ul"+                            }+                        )+                        ( fromList [] )+                        [ TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.idris-lang.org/feeds/all.atom.xml"+                                        )+                                    ,+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "rel"+                                            }+                                        , "alternate"+                                        )+                                    ]+                                )+                                [ TokenTextContent "atom feed" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.twitter.com/idrislang"+                                        )+                                    ]+                                )+                                [ TokenTextContent "@idrislang" ]+                            ]+                        , TokenTag+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "li"+                                }+                            )+                            ( fromList [] )+                            [ TokenTag+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "a"+                                    }+                                )+                                ( fromList+                                    [+                                        ( QName+                                            { namePrefix = ""+                                            , nameLocal = "href"+                                            }+                                        , "https://www.github.com/idris-lang"+                                        )+                                    ]+                                )+                                [ TokenTextContent "GitHub" ]+                            ]+                        , TokenTextContent "+                                                  "+                        ]+                    , TokenTextContent "+                                      "+                    ]+                , TokenTextContent "+                          "+                ]+            , TokenTag+                ( QName+                    { namePrefix = ""+                    , nameLocal = "footer"+                    }+                )+                ( fromList+                    [+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "class"+                            }+                        , "body"+                        )+                    ,+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "id"+                            }+                        , "footer"+                        )+                    ]+                )+                [ TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "address"+                        }+                    )+                    ( fromList+                        [+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "class"+                                }+                            , "vcard body"+                            )+                        ,+                            ( QName+                                { namePrefix = ""+                                , nameLocal = "id"+                                }+                            , "about"+                            )+                        ]+                    )+                    [ TokenTextContent "+                                      Proudly powered by "+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "a"+                            }+                        )+                        ( fromList+                            [+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "href"+                                    }+                                , "http://alexis.notmyidea.org/pelican/"+                                )+                            ]+                        )+                        [ TokenTextContent "Pelican" ]+                    , TokenTextContent ", which takes great advantage of "+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "a"+                            }+                        )+                        ( fromList+                            [+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "href"+                                    }+                                , "http://python.org"+                                )+                            ]+                        )+                        [ TokenTextContent "Python" ]+                    , TokenTextContent " (not Idris :)).+                                      Patches are welcome on "+                    , TokenTag+                        ( QName+                            { namePrefix = ""+                            , nameLocal = "a"+                            }+                        )+                        ( fromList+                            [+                                ( QName+                                    { namePrefix = ""+                                    , nameLocal = "href"+                                    }+                                , "https://github.com/edwinb/idris-lang.org/"+                                )+                            ]+                        )+                        [ TokenTextContent "github" ]+                    , TokenTextContent "!+                                      "+                    ]+                , TokenTag+                    ( QName+                        { namePrefix = ""+                        , nameLocal = "p"+                        }+                    )+                    ( fromList [] )+                    [ TokenTextContent "The theme is «notmyidea-cms», a modified version of «notmyidea», the default theme." ]+                , TokenTextContent "+                          "+                ]+            , TokenTextContent "++              "+            ]+        , TokenTextContent "+          "+        ]+    , TokenTextContent "+      "+    ]

@@ -0,0 +1,2481 @@+Right+    [ TokenDoctype+        ( Doctype "html" Nothing+            ( InternalSubset+                { _elementTypes = []+                , _attributeLists = []+                , _generalEntities = []+                , _parameterEntities = []+                , _notations = []+                , _instructions = []+                }+            )+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "html"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "lang"+                    }+                )+                [ ContentText "en" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "head"+                }+            ) []+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "title"+                }+            ) []+        )+    , TokenData+        [ ContentText "Idris: A Language for Type-Driven Development" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "title"+            }+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenEmptyElementTag+        ( EmptyElementTag+            ( QName+                { namePrefix = ""+                , nameLocal = "meta"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "charset"+                    }+                )+                [ ContentText "utf-8" ]+            ]+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenEmptyElementTag+        ( EmptyElementTag+            ( QName+                { namePrefix = ""+                , nameLocal = "link"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "rel"+                    }+                )+                [ ContentText "stylesheet" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/theme/css/main.css" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "type"+                    }+                )+                [ ContentText "text/css" ]+            ]+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenEmptyElementTag+        ( EmptyElementTag+            ( QName+                { namePrefix = ""+                , nameLocal = "link"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "type"+                    }+                )+                [ ContentText "application/atom+xml" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "rel"+                    }+                )+                [ ContentText "alternate" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "title"+                    }+                )+                [ ContentText "Idris ATOM Feed" ]+            ]+        )+    , TokenData+        [ ContentText "+++                " ]+    , TokenComment "[if IE]>+                      <script src="http://html5shiv.googlecode.com/svn/trunk/html5.js"></script><![endif]"+    , TokenData+        [ ContentText "++                " ]+    , TokenComment "[if lte IE 7]>+                      <link rel="stylesheet" type="text/css" media="all" href="https://www.idris-lang.org/css/ie.css"/>+                      <script src="https://www.idris-lang.org/js/IE8.js" type="text/javascript"></script><![endif]"+    , TokenData+        [ ContentText "++                " ]+    , TokenComment "[if lt IE 7]>+                      <link rel="stylesheet" type="text/css" media="all" href="https://www.idris-lang.org/css/ie6.css"/><![endif]"+    , TokenData+        [ ContentText "++        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "head"+            }+        )+    , TokenData+        [ ContentText "++        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "body"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "index" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "home" ]+            ]+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "header"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "banner" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "body" ]+            ]+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h1"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/index.html" ]+            ]+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenComment "<img src = "https://www.idris-lang.org/images/logo-small.png" alt = "[Idris]" aligh=left>"+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h1"+            }+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "nav"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "ul"+                }+            ) []+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/index.html" ]+            ]+        )+    , TokenData+        [ ContentText "Home" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                            " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/pages/download.html" ]+            ]+        )+    , TokenData+        [ ContentText "Download" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                            " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/pages/example.html" ]+            ]+        )+    , TokenData+        [ ContentText "Example" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                            " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/pages/documentation.html" ]+            ]+        )+    , TokenData+        [ ContentText "Documentation" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenComment " <li><a href="https://www.idris-lang.org/">Archives</a></li> "+    , TokenData+        [ ContentText "+                            " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/category/news.html" ]+            ]+        )+    , TokenData+        [ ContentText "News" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "ul"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "nav"+            }+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "header"+            }+        )+    , TokenComment " /#banner "+    , TokenData+        [ ContentText "+++        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "section"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "content" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "body" ]+            ]+        )+    , TokenData+        [ ContentText "+            " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h1"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "entry-title" ]+            ]+        )+    , TokenData+        [ ContentText "Idris: A Language for Type-Driven Development" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h1"+            }+        )+    , TokenData+        [ ContentText "+            " ]+    , TokenComment " .. image:: images/profile.jpeg "+    , TokenData+        [ ContentText "+        " ]+    , TokenComment " :alt: [Shape Sorter Box] "+    , TokenData+        [ ContentText "+        " ]+    , TokenComment " :align: right "+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "Idris is a programming language designed to encourage " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "em"+                }+            ) []+        )+    , TokenData+        [ ContentText "Type-Driven+        Development" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "em"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "In type-driven development, types are tools for constructing programs.  We+        treat the type as the " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "em"+                }+            ) []+        )+    , TokenData+        [ ContentText "plan" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "em"+            }+        )+    , TokenData+        [ ContentText " for a program, and use the compiler and type+        checker as our assistant, guiding us to a complete program that satisfies the+        type. The more expressive the type is that we give up front, the more+        confidence we can have that the resulting program will be correct." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "In Idris, types are first-class constructs in the langauge. This means types+        can be passed as arguments to functions, and returned from functions just like+        any other value, such as numbers, strings, or lists. This is a small but+        powerful idea, enabling:" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "ul"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "simple" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenData+        [ ContentText "relationships to be expressed between values; for example, that two lists+        have the same length." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenData+        [ ContentText "assumptions to be made explicit and checked by the compiler. For example, if+        you assume that a list is non-empty, Idris can ensure this assumption always+        holds before the program is run." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenData+        [ ContentText "if desired, properties of program behaviour to be formally stated and+        proven." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "ul"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "div"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "section" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "getting-started" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h2"+                }+            ) []+        )+    , TokenData+        [ ContentText "Getting Started" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h2"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "You can see some " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/pages/example.html" ]+            ]+        )+    , TokenData+        [ ContentText "small examples" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText ", then take a+        look at the " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/pages/documentation.html" ]+            ]+        )+    , TokenData+        [ ContentText "documentation" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "div"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "div"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "section" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "community" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h2"+                }+            ) []+        )+    , TokenData+        [ ContentText "Community" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h2"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dl"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "docutils" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dt"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "strong"+                }+            ) []+        )+    , TokenData+        [ ContentText "Mailing list" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "strong"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dt"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dd"+                }+            ) []+        )+    , TokenData+        [ ContentText "Long-form discussion happens on the " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://groups.google.com/forum/#!forum/idris-lang" ]+            ]+        )+    , TokenData+        [ ContentText "mailing list" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dd"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dt"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "strong"+                }+            ) []+        )+    , TokenData+        [ ContentText "IRC" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "strong"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dt"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dd"+                }+            ) []+        )+    , TokenData+        [ ContentText "There is also an irc channel " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "tt"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "docutils literal" ]+            ]+        )+    , TokenData+        [ ContentText "#idris" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "tt"+            }+        )+    , TokenData+        [ ContentText " on " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "irc://chat.freenode.net/idris" ]+            ]+        )+    , TokenData+        [ ContentText "freenode" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText ".+        Point your irc client to " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "tt"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "docutils literal" ]+            ]+        )+    , TokenData+        [ ContentText "chat.freenode.net" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "tt"+            }+        )+    , TokenData+        [ ContentText " then " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "tt"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "docutils literal" ]+            ]+        )+    , TokenData+        [ ContentText "/join #idris" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "tt"+            }+        )+    , TokenData+        [ ContentText ".+        Alternatively, there is a " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "http://webchat.freenode.net/" ]+            ]+        )+    , TokenData+        [ ContentText "web interface" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dd"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dt"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "strong"+                }+            ) []+        )+    , TokenData+        [ ContentText "GitHub" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "strong"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dt"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dd"+                }+            ) []+        )+    , TokenData+        [ ContentText "The Idris source is available from our repository.+        Tools and code by the wider Idris community are available in a+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://github.com/idris-hackers" ]+            ]+        )+    , TokenData+        [ ContentText "GitHub organisation" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dd"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dt"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "strong"+                }+            ) []+        )+    , TokenData+        [ ContentText "Slack" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "strong"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dt"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "dd"+                }+            ) []+        )+    , TokenData+        [ ContentText "There is an active " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "tt"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "docutils literal" ]+            ]+        )+    , TokenData+        [ ContentText "#idris" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "tt"+            }+        )+    , TokenData+        [ ContentText " channel on the+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://functionalprogramming.slack.com/" ]+            ]+        )+    , TokenData+        [ ContentText "Functional Programming" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText " Slack." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dd"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "dl"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "All participants in these forums are requested to abide by the+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/pages/community-standards.html" ]+            ]+        )+    , TokenData+        [ ContentText "community standards" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "Idris development is led by " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "http://www.type-driven.org.uk/edwinb/" ]+            ]+        )+    , TokenData+        [ ContentText "Edwin Brady" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "+        at the " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "http://www.cs.st-andrews.ac.uk" ]+            ]+        )+    , TokenData+        [ ContentText "School of Computer Science, University of St Andrews" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "Many thanks to Heath Johns for designing the logo." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "div"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "div"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "section" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "support" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h2"+                }+            ) []+        )+    , TokenData+        [ ContentText "Support" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h2"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "Idris has been generously supported by the following " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://epsrc.ukri.org/" ]+            ]+        )+    , TokenData+        [ ContentText "EPSRC" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText " grants:" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "ul"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "simple" ]+            ]+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/N024222/1" ]+            ]+        )+    , TokenData+        [ ContentText "Type-driven Verification of Communicating Systems" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/T007265/1" ]+            ]+        )+    , TokenData+        [ ContentText "Programming as Conversation: Type-Driven Development in Action" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "ul"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "We are also grateful for the continuing support+        of " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "reference external" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "http://www.sicsa.ac.uk/" ]+            ]+        )+    , TokenData+        [ ContentText "SICSA" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText ", the Scottish Informatics and Computer Science Alliance" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "div"+            }+        )+    , TokenData+        [ ContentText "++        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "section"+            }+        )+    , TokenData+        [ ContentText "++                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "aside"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "sidebar" ]+            ]+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "div"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "widget" ]+            ]+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h2"+                }+            ) []+        )+    , TokenData+        [ ContentText "Categories" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h2"+            }+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "ul"+                }+            ) []+        )+    , TokenData+        [ ContentText "+                                   " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/category/news.html" ]+            ]+        )+    , TokenData+        [ ContentText "News" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "ul"+            }+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "div"+            }+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "div"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "widget social" ]+            ]+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "h2"+                }+            ) []+        )+    , TokenData+        [ ContentText "Social" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "h2"+            }+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "ul"+                }+            ) []+        )+    , TokenData+        [ ContentText "+                                    " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.idris-lang.org/feeds/all.atom.xml" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "rel"+                    }+                )+                [ ContentText "alternate" ]+            ]+        )+    , TokenData+        [ ContentText "atom feed" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "++                                    " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.twitter.com/idrislang" ]+            ]+        )+    , TokenData+        [ ContentText "@idrislang" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                                    " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "li"+                }+            ) []+        )+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://www.github.com/idris-lang" ]+            ]+        )+    , TokenData+        [ ContentText "GitHub" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "li"+            }+        )+    , TokenData+        [ ContentText "+                                " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "ul"+            }+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "div"+            }+        )+    , TokenComment " /.social "+    , TokenData+        [ ContentText "+                " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "aside"+            }+        )+    , TokenComment " /#sidebar "+    , TokenData+        [ ContentText "++                " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "footer"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "footer" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "body" ]+            ]+        )+    , TokenData+        [ ContentText "+                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "address"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "id"+                    }+                )+                [ ContentText "about" ]+            , Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "class"+                    }+                )+                [ ContentText "vcard body" ]+            ]+        )+    , TokenData+        [ ContentText "+                        Proudly powered by " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "http://alexis.notmyidea.org/pelican/" ]+            ]+        )+    , TokenData+        [ ContentText "Pelican" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText ", which takes great advantage of " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "http://python.org" ]+            ]+        )+    , TokenData+        [ ContentText "Python" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText " (not Idris :)).+                        Patches are welcome on " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "a"+                }+            )+            [ Attribute+                ( QName+                    { namePrefix = ""+                    , nameLocal = "href"+                    }+                )+                [ ContentText "https://github.com/edwinb/idris-lang.org/" ]+            ]+        )+    , TokenData+        [ ContentText "github" ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "a"+            }+        )+    , TokenData+        [ ContentText "!+                        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "address"+            }+        )+    , TokenComment " /#about "+    , TokenData+        [ ContentText "++                        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "p"+                }+            ) []+        )+    , TokenData+        [ ContentText "The theme is «notmyidea-cms», a modified version of «notmyidea», the default theme." ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "p"+            }+        )+    , TokenData+        [ ContentText "+                " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "footer"+            }+        )+    , TokenComment " /#footer "+    , TokenData+        [ ContentText "++        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "body"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "html"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    ]

@@ -0,0 +1,9 @@+<?xml version="1.0" encoding="utf-8"?>+<!DOCTYPE sgml [+  <!ELEMENT sgml ANY>+  <!ENTITY % std       "standard SGML">+  <!ENTITY % signature " &#x2014; &author;.">+  <!ENTITY % question  "Why couldn&#x2019;t I publish my books directly in %std;?">+  <!ENTITY % author    "William Shakespeare">+]>+<sgml>&question;&signature;</sgml>

@@ -0,0 +1,49 @@+Right+    [ TokenProlog+        ( Prolog+            { prologXmlDeclaration = Just+                ( XMLDeclaration "1.0"+                    ( Just "utf-8" ) Nothing+                )+            , prologInstructions = []+            , prologDoctype = Just+                ( Doctype "sgml" Nothing+                    ( InternalSubset+                        { _elementTypes =+                            [ ElementType "sgml" ContentAny ]+                        , _attributeLists = []+                        , _generalEntities = []+                        , _parameterEntities =+                            [ ParameterEntity "std"+                                [ ValueText "standard SGML" ]+                            , ParameterEntity "signature"+                                [ ValueText " "+                                , ValueReference+                                    ( CharRef '\8212' )+                                , ValueText " "+                                , ValueReference+                                    ( EntityRef "author" )+                                , ValueText "."+                                ]+                            , ParameterEntity "question"+                                [ ValueText "Why couldn"+                                , ValueReference+                                    ( CharRef '\8217' )+                                , ValueText "t I publish my books directly in "+                                , ValueParameterEntityRef+                                    ( ParameterEntityRef "std" )+                                , ValueText "?"+                                ]+                            , ParameterEntity "author"+                                [ ValueText "William Shakespeare" ]+                            ]+                        , _notations = []+                        , _instructions = []+                        }+                    )+                )+            }+        )+    , TokenTextContent "+      "+    ]

@@ -0,0 +1,71 @@+Right+    [ TokenXMLDeclaration+        ( XMLDeclaration "1.0"+            ( Just "utf-8" ) Nothing+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenDoctype+        ( Doctype "sgml" Nothing+            ( InternalSubset+                { _elementTypes =+                    [ ElementType "sgml" ContentAny ]+                , _attributeLists = []+                , _generalEntities = []+                , _parameterEntities =+                    [ ParameterEntity "std"+                        [ ValueText "standard SGML" ]+                    , ParameterEntity "signature"+                        [ ValueText " "+                        , ValueReference+                            ( CharRef '\8212' )+                        , ValueText " "+                        , ValueReference+                            ( EntityRef "author" )+                        , ValueText "."+                        ]+                    , ParameterEntity "question"+                        [ ValueText "Why couldn"+                        , ValueReference+                            ( CharRef '\8217' )+                        , ValueText "t I publish my books directly in "+                        , ValueParameterEntityRef+                            ( ParameterEntityRef "std" )+                        , ValueText "?"+                        ]+                    , ParameterEntity "author"+                        [ ValueText "William Shakespeare" ]+                    ]+                , _notations = []+                , _instructions = []+                }+            )+        )+    , TokenData+        [ ContentText "+        " ]+    , TokenStartTag+        ( StartTag+            ( QName+                { namePrefix = ""+                , nameLocal = "sgml"+                }+            ) []+        )+    , TokenData+        [ ContentReference+            ( EntityRef "question" )+        , ContentReference+            ( EntityRef "signature" )+        ]+    , TokenEndTag+        ( QName+            { namePrefix = ""+            , nameLocal = "sgml"+            }+        )+    , TokenData+        [ ContentText "+        " ]+    ]