{-# 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)
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
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")
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 [] = []
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>"]
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)
]
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
}
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"]
}
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
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))
-> (() -> 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