{-# LANGUAGE BlockArguments #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-name-shadowing #-} module Blagda.Markdown where import Blagda.Agda import Blagda.Equations (hideSteps) import Blagda.Latex import Blagda.References (linkDocument) import Blagda.Types import Control.Monad.IO.Class import qualified Data.ByteString.Lazy as LazyBS import Data.Digest.Pure.SHA import Data.Map.Lazy (Map) import qualified Data.Map.Lazy as Map import Data.Maybe import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Text.Encoding as Text import qualified Data.Text.IO as Text import Development.Shake import Development.Shake.FilePath import Network.URI.Encode (decodeText) import qualified System.Directory as Dir import Text.HTML.TagSoup import Text.Pandoc import Text.Pandoc.Walk data Reference = Reference { refHref :: Text , refClasses :: [Text] } deriving (Eq, Show) ------------------------------------------------------------------------------ -- | 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. loadMarkdown :: (Meta -> a) -> String -> FilePath -> Action (Post Pandoc a) loadMarkdown f commit input = do let url = dropExtension (dropDirectory1 input) <.> "html" modname = moduleName (dropDirectory1 (dropDirectory1 (dropExtension input))) permalink = commit input title | length modname > 24 = '…':reverse (take 24 (reverse modname)) | otherwise = modname Pandoc meta markdown <- liftIO do contents <- Text.readFile input either (fail . show) pure =<< runIO do md <- readMarkdown def { readerExtensions = getDefaultExtensions "markdown" } [(input, contents)] pure md -- applyFilters def [JSONFilter "agda-reference-filter"] ["html"] md let liftIO $ Dir.createDirectoryIfMissing False "_build/diagrams" markdown <- pure . walk patchInlines . Pandoc (patchMeta title permalink meta) $ markdown markdown <- walkM patchInline markdown markdown <- walkM patchBlock markdown markdown <- pure $ linkDocument markdown pure $ Post { p_path = url , p_contents = markdown , p_meta = f meta } htmlInl :: Text -> Inline htmlInl = RawInline (Format "html") -- | Replace any expression $foo$-bar with $foo$-bar, so that -- the equation is not split when word wrapping. patchInlines :: [Inline] -> [Inline] patchInlines (m@Math{}:s@(Str txt):xs) | not (Text.isPrefixOf " " txt) = htmlInl "" : m : s : htmlInl "" : patchInlines xs patchInlines (x:xs) = x:patchInlines xs patchInlines [] = [] -- Make all headers links, and add an anchor emoji. patchBlock :: MonadIO f => Block -> f Block patchBlock (Header i a@(ident, _, _) inl) = pure $ Header i a $ htmlInl (Text.concat [""]) : inl ++ [htmlInl "🔗"] -- Replace quiver code blocks with a link to an SVG file, and depend on the SVG file. patchBlock (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` classes = do let digest = showDigest . sha1 . LazyBS.fromStrict $ Text.encodeUtf8 contents title = fromMaybe "commutative diagram" (lookup "title" attrs) writeFile' ("_build/diagrams" digest <.> "tex") $ Text.unpack contents pure $ Div ("", ["diagram-container"], []) [ Plain [ Image (id, "diagram":classes, attrs) [] (Text.pack (digest <.> "svg"), title) ] ] patchBlock h = pure h patchInline :: Inline -> Action Inline patchInline (Math DisplayMath contents) = htmlInl <$> buildLatexEqn True contents patchInline (Math InlineMath contents) = htmlInl <$> buildLatexEqn False contents patchInline h = pure h mStr :: String -> MetaValue mStr = MetaString . Text.pack patchMeta :: String -> String -> Meta -> Meta patchMeta title permalink (Meta m) = Meta $ m <> Map.fromList [ ("title", mStr title) , ("source", mStr permalink) ] -- | Parse an Agda module (in the final build directory) to find a list -- of its definitions. parseFileIdents :: Text -> Action (Map Text Reference, Map Text Text) parseFileIdents mdl = do let path = "_build/html1" Text.unpack mdl <.> "html" need [ path ] traced ("parsing " ++ Text.unpack mdl) do go mempty mempty . parseTags <$> Text.readFile path where go fwd rev (TagOpen "a" attrs:TagText name:TagClose "a":xs) | Just id <- lookup "id" attrs, Just href <- lookup "href" attrs , Just classes <- lookup "class" attrs , mdl `Text.isPrefixOf` href, id `Text.isSuffixOf` href = go (Map.insert name (Reference href (Text.words classes)) fwd) (Map.insert href name rev) xs | Just classes <- lookup "class" attrs, Just href <- lookup "href" attrs , "Module" `elem` Text.words classes, mdl `Text.isPrefixOf` href = go (Map.insert name (Reference href (Text.words classes)) fwd) (Map.insert href name rev) xs go fwd rev (_:xs) = go fwd rev xs go fwd rev [] = (fwd, rev) defaultWriterOptions :: WriterOptions defaultWriterOptions = def { writerExtensions = getDefaultExtensions "html" } renderPost :: (Text -> Action (Map Text Reference, Map Text Text)) -> WriterOptions -> Post Pandoc a -> Action (Post Text a) renderPost fileIdents options po = do text <- liftIO $ either (fail . show) pure =<< runIO do writeHtml5String options $ p_contents po tags <- traverse (parseAgdaLink fileIdents) $ parseTags text pure $ po { p_path = dropExtension (p_path po) <.> "html" , p_contents = renderHTML5 $ hideSteps False tags } -- writeTemplate :: FilePath -> Context Text -> (Text -> Action (Map Text Reference, Map Text Text)) -> Pandoc -> FilePath -> Action () -- writeTemplate templateName context fileIdents markdown output = do -- text <- liftIO $ either (fail . show) pure =<< runIO do -- template <- getTemplate templateName >>= runWithPartials . compileTemplate templateName -- >>= either (throwError . PandocTemplateError . Text.pack) pure -- let -- options = def { writerTemplate = Just template -- , writerTableOfContents = True -- , writerVariables = context -- , writerExtensions = getDefaultExtensions "html" } -- writeHtml5String options markdown -- tags <- traverse (parseAgdaLink fileIdents) $ parseTags text -- writeFile' output $ Text.unpack $ renderHTML5 $ hideSteps False tags renderHTML5 :: [Tag Text] -> Text renderHTML5 = renderTagsOptions renderOptions { optMinimize = flip elem ["br", "meta", "link", "img", "hr"] } -- command_ [] "agda-fold-equations" [output] -- | Possibly interpret an link to be a honest-to-god -- link to the definition. parseAgdaLink :: (Text -> Action (Map Text Reference, Map Text Text)) -> Tag Text -> Action (Tag Text) parseAgdaLink fileIds (TagOpen "a" attrs) | Just href <- lookup "href" attrs, Text.pack "agda://" `Text.isPrefixOf` href = let href' = Text.splitOn "#" $ Text.drop (Text.length "agda://") href cont mdl ident = do (idMap, _) <- fileIds mdl case Map.lookup ident idMap of Just (Reference href'' _) -> do pure (TagOpen "a" (emplace [("href", href'')] attrs)) _ -> error $ "Could not compile Agda link: " ++ show href' in case href' of [mdl] -> cont mdl mdl [mdl, ident] -> cont mdl (decodeText ident) _ -> error $ "Could not parse Agda link: " ++ show href parseAgdaLink _ x = pure x emplace :: Eq a => [(a, b)] -> [(a, b)] -> [(a, b)] emplace ((p, x) : xs) ys = (p, x) : emplace xs (filter ((/= p) . fst) ys) emplace [] ys = ys -- | Lookup an identifier given a module name and ID within that module, -- returning its type. addLinkType :: (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) addLinkType fileIds fileTys tag@(TagOpen "a" attrs) | Just href <- lookup "href" attrs , [mdl, _] <- Text.splitOn ".html#" href = do case Text.isInfixOf "/" mdl of True -> pure tag False -> do ty <- resolveId mdl href <$> fileIds mdl <*> fileTys () pure $ case ty of Nothing -> tag Just ty -> TagOpen "a" (emplace [("data-type", ty)] attrs) where resolveId _ href (_, _) types = Map.lookup href types addLinkType _ _ x = pure x