{-# 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
  { Reference -> Text
refHref :: Text
  , Reference -> [Text]
refClasses :: [Text]
  } deriving (Reference -> Reference -> Bool
(Reference -> Reference -> Bool)
-> (Reference -> Reference -> Bool) -> Eq Reference
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Reference -> Reference -> Bool
$c/= :: Reference -> Reference -> Bool
== :: Reference -> Reference -> Bool
$c== :: Reference -> Reference -> Bool
Eq, Int -> Reference -> ShowS
[Reference] -> ShowS
Reference -> String
(Int -> Reference -> ShowS)
-> (Reference -> String)
-> ([Reference] -> ShowS)
-> Show Reference
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Reference] -> ShowS
$cshowList :: [Reference] -> ShowS
show :: Reference -> String
$cshow :: Reference -> String
showsPrec :: Int -> Reference -> ShowS
$cshowsPrec :: Int -> Reference -> ShowS
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 :: (Meta -> a) -> String -> String -> Action (Post Pandoc a)
loadMarkdown Meta -> a
f String
commit String
input = do
  let url :: String
url = ShowS
dropExtension (ShowS
dropDirectory1 String
input) String -> ShowS
<.> String
"html"
      modname :: String
modname = ShowS
moduleName (ShowS
dropDirectory1 (ShowS
dropDirectory1 (ShowS
dropExtension String
input)))
      permalink :: String
permalink = String
commit String -> ShowS
</> String
input

      title :: String
title
        | String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
modname Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
24 = Char
'…'Char -> ShowS
forall a. a -> [a] -> [a]
:ShowS
forall a. [a] -> [a]
reverse (Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
24 (ShowS
forall a. [a] -> [a]
reverse String
modname))
        | Bool
otherwise = String
modname

  Pandoc Meta
meta [Block]
markdown <- IO Pandoc -> Action Pandoc
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO do
    Text
contents <- String -> IO Text
Text.readFile String
input
    (PandocError -> IO Pandoc)
-> (Pandoc -> IO Pandoc) -> Either PandocError Pandoc -> IO Pandoc
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> IO Pandoc
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO Pandoc)
-> (PandocError -> String) -> PandocError -> IO Pandoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PandocError -> String
forall a. Show a => a -> String
show) Pandoc -> IO Pandoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either PandocError Pandoc -> IO Pandoc)
-> IO (Either PandocError Pandoc) -> IO Pandoc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PandocIO Pandoc -> IO (Either PandocError Pandoc)
forall a. PandocIO a -> IO (Either PandocError a)
runIO do
      Pandoc
md <- ReaderOptions -> [(String, Text)] -> PandocIO Pandoc
forall (m :: * -> *) a.
(PandocMonad m, ToSources a) =>
ReaderOptions -> a -> m Pandoc
readMarkdown ReaderOptions
forall a. Default a => a
def { readerExtensions :: Extensions
readerExtensions = Text -> Extensions
getDefaultExtensions Text
"markdown" } [(String
input, Text
contents)]
      Pandoc -> PandocIO Pandoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pandoc
md
      -- applyFilters def [JSONFilter "agda-reference-filter"] ["html"] md

  let
  IO () -> Action ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Action ()) -> IO () -> Action ()
forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
Dir.createDirectoryIfMissing Bool
False String
"_build/diagrams"

  Pandoc
markdown <- Pandoc -> Action Pandoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pandoc -> Action Pandoc)
-> ([Block] -> Pandoc) -> [Block] -> Action Pandoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Inline] -> [Inline]) -> Pandoc -> Pandoc
forall a b. Walkable a b => (a -> a) -> b -> b
walk [Inline] -> [Inline]
patchInlines (Pandoc -> Pandoc) -> ([Block] -> Pandoc) -> [Block] -> Pandoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Meta -> [Block] -> Pandoc
Pandoc (String -> String -> Meta -> Meta
patchMeta String
title String
permalink Meta
meta) ([Block] -> Action Pandoc) -> [Block] -> Action Pandoc
forall a b. (a -> b) -> a -> b
$ [Block]
markdown
  Pandoc
markdown <- (Inline -> Action Inline) -> Pandoc -> Action Pandoc
forall a b (m :: * -> *).
(Walkable a b, Monad m, Applicative m, Functor m) =>
(a -> m a) -> b -> m b
walkM Inline -> Action Inline
patchInline Pandoc
markdown
  Pandoc
markdown <- (Block -> Action Block) -> Pandoc -> Action Pandoc
forall a b (m :: * -> *).
(Walkable a b, Monad m, Applicative m, Functor m) =>
(a -> m a) -> b -> m b
walkM Block -> Action Block
forall (f :: * -> *). MonadIO f => Block -> f Block
patchBlock Pandoc
markdown
  Pandoc
markdown <- Pandoc -> Action Pandoc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pandoc -> Action Pandoc) -> Pandoc -> Action Pandoc
forall a b. (a -> b) -> a -> b
$ Pandoc -> Pandoc
linkDocument Pandoc
markdown

  Post Pandoc a -> Action (Post Pandoc a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Post Pandoc a -> Action (Post Pandoc a))
-> Post Pandoc a -> Action (Post Pandoc a)
forall a b. (a -> b) -> a -> b
$ Post :: forall contents meta.
String -> contents -> meta -> Post contents meta
Post
    { p_path :: String
p_path = String
url
    , p_contents :: Pandoc
p_contents = Pandoc
markdown
    , p_meta :: a
p_meta = Meta -> a
f Meta
meta
    }



htmlInl :: Text -> Inline
htmlInl :: Text -> Inline
htmlInl = Format -> Text -> Inline
RawInline (Text -> Format
Format Text
"html")


-- | Replace any expression $foo$-bar with <span ...>$foo$-bar</span>, so that
-- the equation is not split when word wrapping.
patchInlines :: [Inline] -> [Inline]
patchInlines :: [Inline] -> [Inline]
patchInlines (m :: Inline
m@Math{}:s :: Inline
s@(Str Text
txt):[Inline]
xs)
  | Bool -> Bool
not (Text -> Text -> Bool
Text.isPrefixOf Text
" " Text
txt)
  = Text -> Inline
htmlInl Text
"<span style=\"white-space: nowrap;\">" Inline -> [Inline] -> [Inline]
forall a. a -> [a] -> [a]
: Inline
m Inline -> [Inline] -> [Inline]
forall a. a -> [a] -> [a]
: Inline
s Inline -> [Inline] -> [Inline]
forall a. a -> [a] -> [a]
: Text -> Inline
htmlInl Text
"</span>"
  Inline -> [Inline] -> [Inline]
forall a. a -> [a] -> [a]
: [Inline] -> [Inline]
patchInlines [Inline]
xs
patchInlines (Inline
x:[Inline]
xs) = Inline
xInline -> [Inline] -> [Inline]
forall a. a -> [a] -> [a]
:[Inline] -> [Inline]
patchInlines [Inline]
xs
patchInlines [] = []


-- Make all headers links, and add an anchor emoji.
patchBlock :: MonadIO f => Block -> f Block
patchBlock :: Block -> f Block
patchBlock (Header Int
i a :: Attr
a@(Text
ident, [Text]
_, [(Text, Text)]
_) [Inline]
inl) = Block -> f Block
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Block -> f Block) -> Block -> f Block
forall a b. (a -> b) -> a -> b
$ Int -> Attr -> [Inline] -> Block
Header Int
i Attr
a
  ([Inline] -> Block) -> [Inline] -> Block
forall a b. (a -> b) -> a -> b
$ Text -> Inline
htmlInl ([Text] -> Text
Text.concat [Text
"<a href=\"#", Text
ident, Text
"\" class=\"header-link\">"])
  Inline -> [Inline] -> [Inline]
forall a. a -> [a] -> [a]
: [Inline]
inl
  [Inline] -> [Inline] -> [Inline]
forall a. [a] -> [a] -> [a]
++ [Text -> Inline
htmlInl Text
"<span class=\"header-link-emoji\">🔗</span></a>"]
-- Replace quiver code blocks with a link to an SVG file, and depend on the SVG file.
patchBlock (CodeBlock (Text
id, [Text]
classes, [(Text, Text)]
attrs) Text
contents) | Text
"quiver" Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
classes = do
  let
    digest :: String
digest = Digest SHA1State -> String
forall t. Digest t -> String
showDigest (Digest SHA1State -> String)
-> (ByteString -> Digest SHA1State) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Digest SHA1State
sha1 (ByteString -> Digest SHA1State)
-> (ByteString -> ByteString) -> ByteString -> Digest SHA1State
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
LazyBS.fromStrict (ByteString -> String) -> ByteString -> String
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
Text.encodeUtf8 Text
contents
    title :: Text
title = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"commutative diagram" (Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"title" [(Text, Text)]
attrs)
  String -> String -> f ()
forall (m :: * -> *).
(MonadIO m, Partial) =>
String -> String -> m ()
writeFile' (String
"_build/diagrams" String -> ShowS
</> String
digest String -> ShowS
<.> String
"tex") (String -> f ()) -> String -> f ()
forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
contents

  Block -> f Block
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Block -> f Block) -> Block -> f Block
forall a b. (a -> b) -> a -> b
$ Attr -> [Block] -> Block
Div (Text
"", [Text
"diagram-container"], [])
    [ [Inline] -> Block
Plain [ Attr -> [Inline] -> (Text, Text) -> Inline
Image (Text
id, Text
"diagram"Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
classes, [(Text, Text)]
attrs) [] (String -> Text
Text.pack (String
digest String -> ShowS
<.> String
"svg"), Text
title) ]
    ]
patchBlock Block
h = Block -> f Block
forall (f :: * -> *) a. Applicative f => a -> f a
pure Block
h


patchInline :: Inline -> Action Inline
patchInline :: Inline -> Action Inline
patchInline (Math MathType
DisplayMath Text
contents) = Text -> Inline
htmlInl (Text -> Inline) -> Action Text -> Action Inline
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Text -> Action Text
buildLatexEqn Bool
True Text
contents
patchInline (Math MathType
InlineMath Text
contents) = Text -> Inline
htmlInl (Text -> Inline) -> Action Text -> Action Inline
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Text -> Action Text
buildLatexEqn Bool
False Text
contents
patchInline Inline
h = Inline -> Action Inline
forall (f :: * -> *) a. Applicative f => a -> f a
pure Inline
h


mStr :: String -> MetaValue
mStr :: String -> MetaValue
mStr = Text -> MetaValue
MetaString (Text -> MetaValue) -> (String -> Text) -> String -> MetaValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack


patchMeta :: String -> String -> Meta -> Meta
patchMeta :: String -> String -> Meta -> Meta
patchMeta String
title String
permalink (Meta Map Text MetaValue
m) =
  Map Text MetaValue -> Meta
Meta (Map Text MetaValue -> Meta) -> Map Text MetaValue -> Meta
forall a b. (a -> b) -> a -> b
$ Map Text MetaValue
m Map Text MetaValue -> Map Text MetaValue -> Map Text MetaValue
forall a. Semigroup a => a -> a -> a
<> [(Text, MetaValue)] -> Map Text MetaValue
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Text
"title", String -> MetaValue
mStr String
title)
                           , (Text
"source", String -> MetaValue
mStr String
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 :: Text -> Action (Map Text Reference, Map Text Text)
parseFileIdents Text
mdl =
  do
    let path :: String
path = String
"_build/html1" String -> ShowS
</> Text -> String
Text.unpack Text
mdl String -> ShowS
<.> String
"html"
    Partial => [String] -> Action ()
[String] -> Action ()
need [ String
path ]
    String
-> IO (Map Text Reference, Map Text Text)
-> Action (Map Text Reference, Map Text Text)
forall a. String -> IO a -> Action a
traced (String
"parsing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
mdl) do
      Map Text Reference
-> Map Text Text
-> [Tag Text]
-> (Map Text Reference, Map Text Text)
go Map Text Reference
forall a. Monoid a => a
mempty Map Text Text
forall a. Monoid a => a
mempty ([Tag Text] -> (Map Text Reference, Map Text Text))
-> (Text -> [Tag Text])
-> Text
-> (Map Text Reference, Map Text Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Tag Text]
forall str. StringLike str => str -> [Tag str]
parseTags (Text -> (Map Text Reference, Map Text Text))
-> IO Text -> IO (Map Text Reference, Map Text Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO Text
Text.readFile String
path
  where
    go :: Map Text Reference
-> Map Text Text
-> [Tag Text]
-> (Map Text Reference, Map Text Text)
go Map Text Reference
fwd Map Text Text
rev (TagOpen Text
"a" [(Text, Text)]
attrs:TagText Text
name:TagClose Text
"a":[Tag Text]
xs)
      | Just Text
id <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"id" [(Text, Text)]
attrs, Just Text
href <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"href" [(Text, Text)]
attrs
      , Just Text
classes <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"class" [(Text, Text)]
attrs
      , Text
mdl Text -> Text -> Bool
`Text.isPrefixOf` Text
href, Text
id Text -> Text -> Bool
`Text.isSuffixOf` Text
href
      = Map Text Reference
-> Map Text Text
-> [Tag Text]
-> (Map Text Reference, Map Text Text)
go (Text -> Reference -> Map Text Reference -> Map Text Reference
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name (Text -> [Text] -> Reference
Reference Text
href (Text -> [Text]
Text.words Text
classes)) Map Text Reference
fwd)
           (Text -> Text -> Map Text Text -> Map Text Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
href Text
name Map Text Text
rev) [Tag Text]
xs
      | Just Text
classes <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"class" [(Text, Text)]
attrs, Just Text
href <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"href" [(Text, Text)]
attrs
      , Text
"Module" Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Text -> [Text]
Text.words Text
classes, Text
mdl Text -> Text -> Bool
`Text.isPrefixOf` Text
href
      = Map Text Reference
-> Map Text Text
-> [Tag Text]
-> (Map Text Reference, Map Text Text)
go (Text -> Reference -> Map Text Reference -> Map Text Reference
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name (Text -> [Text] -> Reference
Reference Text
href (Text -> [Text]
Text.words Text
classes)) Map Text Reference
fwd)
           (Text -> Text -> Map Text Text -> Map Text Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
href Text
name Map Text Text
rev) [Tag Text]
xs
    go Map Text Reference
fwd Map Text Text
rev (Tag Text
_:[Tag Text]
xs) = Map Text Reference
-> Map Text Text
-> [Tag Text]
-> (Map Text Reference, Map Text Text)
go Map Text Reference
fwd Map Text Text
rev [Tag Text]
xs
    go Map Text Reference
fwd Map Text Text
rev [] = (Map Text Reference
fwd, Map Text Text
rev)


defaultWriterOptions :: WriterOptions
defaultWriterOptions :: WriterOptions
defaultWriterOptions = WriterOptions
forall a. Default a => a
def
  { writerExtensions :: Extensions
writerExtensions = Text -> Extensions
getDefaultExtensions Text
"html"
  }

renderPost
    :: (Text -> Action (Map Text Reference, Map Text Text))
    -> WriterOptions
    -> Post Pandoc a
    -> Action (Post Text a)
renderPost :: (Text -> Action (Map Text Reference, Map Text Text))
-> WriterOptions -> Post Pandoc a -> Action (Post Text a)
renderPost Text -> Action (Map Text Reference, Map Text Text)
fileIdents WriterOptions
options Post Pandoc a
po = do
  Text
text <- IO Text -> Action Text
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Text -> Action Text) -> IO Text -> Action Text
forall a b. (a -> b) -> a -> b
$ (PandocError -> IO Text)
-> (Text -> IO Text) -> Either PandocError Text -> IO Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> IO Text
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO Text)
-> (PandocError -> String) -> PandocError -> IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PandocError -> String
forall a. Show a => a -> String
show) Text -> IO Text
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either PandocError Text -> IO Text)
-> IO (Either PandocError Text) -> IO Text
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PandocIO Text -> IO (Either PandocError Text)
forall a. PandocIO a -> IO (Either PandocError a)
runIO do
    WriterOptions -> Pandoc -> PandocIO Text
forall (m :: * -> *).
PandocMonad m =>
WriterOptions -> Pandoc -> m Text
writeHtml5String WriterOptions
options (Pandoc -> PandocIO Text) -> Pandoc -> PandocIO Text
forall a b. (a -> b) -> a -> b
$ Post Pandoc a -> Pandoc
forall contents meta. Post contents meta -> contents
p_contents Post Pandoc a
po
  [Tag Text]
tags <- (Tag Text -> Action (Tag Text)) -> [Tag Text] -> Action [Tag Text]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Text -> Action (Map Text Reference, Map Text Text))
-> Tag Text -> Action (Tag Text)
parseAgdaLink Text -> Action (Map Text Reference, Map Text Text)
fileIdents) ([Tag Text] -> Action [Tag Text])
-> [Tag Text] -> Action [Tag Text]
forall a b. (a -> b) -> a -> b
$ Text -> [Tag Text]
forall str. StringLike str => str -> [Tag str]
parseTags Text
text
  Post Text a -> Action (Post Text a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Post Text a -> Action (Post Text a))
-> Post Text a -> Action (Post Text a)
forall a b. (a -> b) -> a -> b
$ Post Pandoc a
po
    { p_path :: String
p_path = ShowS
dropExtension (Post Pandoc a -> String
forall contents meta. Post contents meta -> String
p_path Post Pandoc a
po) String -> ShowS
<.> String
"html"
    , p_contents :: Text
p_contents = [Tag Text] -> Text
renderHTML5 ([Tag Text] -> Text) -> [Tag Text] -> Text
forall a b. (a -> b) -> a -> b
$ Bool -> [Tag Text] -> [Tag Text]
hideSteps Bool
False [Tag Text]
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 :: [Tag Text] -> Text
renderHTML5 = RenderOptions Text -> [Tag Text] -> Text
forall str. StringLike str => RenderOptions str -> [Tag str] -> str
renderTagsOptions RenderOptions Text
forall str. StringLike str => RenderOptions str
renderOptions
  { optMinimize :: Text -> Bool
optMinimize = (Text -> [Text] -> Bool) -> [Text] -> Text -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Text
"br", Text
"meta", Text
"link", Text
"img", Text
"hr"]
  }

  -- command_ [] "agda-fold-equations" [output]


-- | Possibly interpret an <a href="agda://"> 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 :: (Text -> Action (Map Text Reference, Map Text Text))
-> Tag Text -> Action (Tag Text)
parseAgdaLink Text -> Action (Map Text Reference, Map Text Text)
fileIds (TagOpen Text
"a" [(Text, Text)]
attrs)
  | Just Text
href <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"href" [(Text, Text)]
attrs, String -> Text
Text.pack String
"agda://" Text -> Text -> Bool
`Text.isPrefixOf` Text
href =
    let
      href' :: [Text]
href' = Text -> Text -> [Text]
Text.splitOn Text
"#" (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
Text.drop (Text -> Int
Text.length Text
"agda://") Text
href
      cont :: Text -> Text -> Action (Tag Text)
cont Text
mdl Text
ident = do
        (Map Text Reference
idMap, Map Text Text
_) <- Text -> Action (Map Text Reference, Map Text Text)
fileIds Text
mdl
        case Text -> Map Text Reference -> Maybe Reference
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
ident Map Text Reference
idMap of
          Just (Reference Text
href'' [Text]
_) -> do
            Tag Text -> Action (Tag Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> [(Text, Text)] -> Tag Text
forall str. str -> [Attribute str] -> Tag str
TagOpen Text
"a" ([(Text, Text)] -> [(Text, Text)] -> [(Text, Text)]
forall a b. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
emplace [(Text
"href", Text
href'')] [(Text, Text)]
attrs))
          Maybe Reference
_ -> String -> Action (Tag Text)
forall a. Partial => String -> a
error (String -> Action (Tag Text)) -> String -> Action (Tag Text)
forall a b. (a -> b) -> a -> b
$ String
"Could not compile Agda link: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Text] -> String
forall a. Show a => a -> String
show [Text]
href'
     in case [Text]
href' of
          [Text
mdl] -> Text -> Text -> Action (Tag Text)
cont Text
mdl Text
mdl
          [Text
mdl, Text
ident] -> Text -> Text -> Action (Tag Text)
cont Text
mdl (Text -> Text
decodeText Text
ident)
          [Text]
_ -> String -> Action (Tag Text)
forall a. Partial => String -> a
error (String -> Action (Tag Text)) -> String -> Action (Tag Text)
forall a b. (a -> b) -> a -> b
$ String
"Could not parse Agda link: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
forall a. Show a => a -> String
show Text
href
parseAgdaLink Text -> Action (Map Text Reference, Map Text Text)
_ Tag Text
x = Tag Text -> Action (Tag Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag Text
x


emplace :: Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
emplace :: [(a, b)] -> [(a, b)] -> [(a, b)]
emplace ((a
p, b
x) : [(a, b)]
xs) [(a, b)]
ys = (a
p, b
x) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
forall a b. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
emplace [(a, b)]
xs (((a, b) -> Bool) -> [(a, b)] -> [(a, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
p) (a -> Bool) -> ((a, b) -> a) -> (a, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst) [(a, b)]
ys)
emplace [] [(a, b)]
ys = [(a, b)]
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 :: (Text -> Action (Map Text Reference, Map Text Text))
-> (() -> Action (Map Text Text)) -> Tag Text -> Action (Tag Text)
addLinkType Text -> Action (Map Text Reference, Map Text Text)
fileIds () -> Action (Map Text Text)
fileTys tag :: Tag Text
tag@(TagOpen Text
"a" [(Text, Text)]
attrs)
  | Just Text
href <- Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
"href" [(Text, Text)]
attrs
  , [Text
mdl, Text
_] <- Text -> Text -> [Text]
Text.splitOn Text
".html#" Text
href = do
    case Text -> Text -> Bool
Text.isInfixOf Text
"/" Text
mdl of
      Bool
True -> Tag Text -> Action (Tag Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag Text
tag
      Bool
False -> do
        Maybe Text
ty <- Text
-> Text
-> (Map Text Reference, Map Text Text)
-> Map Text Text
-> Maybe Text
forall k p a b a. Ord k => p -> k -> (a, b) -> Map k a -> Maybe a
resolveId Text
mdl Text
href ((Map Text Reference, Map Text Text)
 -> Map Text Text -> Maybe Text)
-> Action (Map Text Reference, Map Text Text)
-> Action (Map Text Text -> Maybe Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Action (Map Text Reference, Map Text Text)
fileIds Text
mdl Action (Map Text Text -> Maybe Text)
-> Action (Map Text Text) -> Action (Maybe Text)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Action (Map Text Text)
fileTys ()
        Tag Text -> Action (Tag Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag Text -> Action (Tag Text)) -> Tag Text -> Action (Tag Text)
forall a b. (a -> b) -> a -> b
$ case Maybe Text
ty of
          Maybe Text
Nothing -> Tag Text
tag
          Just Text
ty -> Text -> [(Text, Text)] -> Tag Text
forall str. str -> [Attribute str] -> Tag str
TagOpen Text
"a" ([(Text, Text)] -> [(Text, Text)] -> [(Text, Text)]
forall a b. Eq a => [(a, b)] -> [(a, b)] -> [(a, b)]
emplace [(Text
"data-type", Text
ty)] [(Text, Text)]
attrs)

    where
      resolveId :: p -> k -> (a, b) -> Map k a -> Maybe a
resolveId p
_ k
href (a
_, b
_) Map k a
types = k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
href Map k a
types
addLinkType Text -> Action (Map Text Reference, Map Text Text)
_ () -> Action (Map Text Text)
_ Tag Text
x = Tag Text -> Action (Tag Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag Text
x