Blagda.Markdown

Documentation

data Reference

Constructors

Reference

Fields

• refHref :: Text
• refClasses :: [Text]

Instances

Eq Reference

Defined in Blagda.Markdown

Methods

(==) :: Reference -> Reference -> Bool

(/=) :: Reference -> Reference -> Bool

Show Reference

Defined in Blagda.Markdown

Methods

showsPrec :: Int -> Reference -> ShowS

show :: Reference -> String

showList :: [Reference] -> ShowS

loadMarkdown :: (Meta -> a) -> String -> FilePath -> Action (Post Pandoc a)

The return type here is whether or not this markdown file is a BLOG POST. Even if it isn't, the file still gets generated.

htmlInl :: Text -> Inline

patchInlines :: [Inline] -> [Inline]

Replace any expression $foo$-bar with ...$foo$-bar/span, so that the equation is not split when word wrapping.

patchBlock :: MonadIO f => Block -> f Block

patchInline :: Inline -> Action Inline

mStr :: String -> MetaValue

patchMeta :: String -> String -> Meta -> Meta

parseFileIdents :: Text -> Action (Map Text Reference, Map Text Text)

Parse an Agda module (in the final build directory) to find a list of its definitions.

defaultWriterOptions :: WriterOptions

renderPost :: (Text -> Action (Map Text Reference, Map Text Text)) -> WriterOptions -> Post Pandoc a -> Action (Post Text a)

renderHTML5 :: [Tag Text] -> Text

parseAgdaLink :: (Text -> Action (Map Text Reference, Map Text Text)) -> Tag Text -> Action (Tag Text)

Possibly interpret an href="agda://" link to be a honest-to-god link to the definition.

emplace :: Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]

addLinkType

Arguments

:: (Text -> Action (Map Text Reference, Map Text Text))

Lookup an ident from a module name and location

-> (() -> Action (Map Text Text))

Lookup a type from a module name and ident

-> Tag Text

-> Action (Tag Text)

Lookup an identifier given a module name and ID within that module, returning its type.