module Agda.Interaction.Highlighting.HTML
( generateHTML
, defaultCSSFile
, generateHTMLWithPageGen
, generatePage
, page
, tokenStream
, code
) where
import Prelude hiding ((!!), concatMap)
import Control.Monad
import Control.Monad.Trans
import Data.Function
import Data.Foldable (toList, concatMap)
import Data.Maybe
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import qualified Data.List as List
import Data.List.Split (splitWhen, chunksOf)
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
import qualified Network.URI.Encode
import System.FilePath
import System.Directory
import Text.Blaze.Html5 hiding (code, map, title)
import qualified Text.Blaze.Html5 as Html5
import Text.Blaze.Html5.Attributes as Attr
import Text.Blaze.Html.Renderer.Text
import Paths_Agda
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Precise
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Common
import Agda.TypeChecking.Monad (TCM, useTC)
import qualified Agda.TypeChecking.Monad as TCM
import Agda.Utils.FileName (filePath)
import Agda.Utils.Function
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Pretty
import Agda.Utils.Impossible
defaultCSSFile :: FilePath
defaultCSSFile :: FilePath
defaultCSSFile = "Agda.css"
rstDelimiter :: String
rstDelimiter :: FilePath
rstDelimiter = ".. raw:: html\n"
highlightOnlyCode :: HtmlHighlight -> FileType -> Bool
highlightOnlyCode :: HtmlHighlight -> FileType -> Bool
highlightOnlyCode HighlightAll _ = Bool
False
highlightOnlyCode HighlightCode _ = Bool
True
highlightOnlyCode HighlightAuto AgdaFileType = Bool
False
highlightOnlyCode HighlightAuto MdFileType = Bool
True
highlightOnlyCode HighlightAuto RstFileType = Bool
True
highlightOnlyCode HighlightAuto OrgFileType = Bool
True
highlightOnlyCode HighlightAuto TexFileType = Bool
False
highlightedFileExt :: HtmlHighlight -> FileType -> String
highlightedFileExt :: HtmlHighlight -> FileType -> FilePath
highlightedFileExt hh :: HtmlHighlight
hh ft :: FileType
ft
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ HtmlHighlight -> FileType -> Bool
highlightOnlyCode HtmlHighlight
hh FileType
ft = "html"
| Bool
otherwise = case FileType
ft of
AgdaFileType -> "html"
MdFileType -> "md"
RstFileType -> "rst"
TexFileType -> "tex"
OrgFileType -> "org"
type PageGen = FilePath
-> FileType
-> Bool
-> String
-> C.TopLevelModuleName
-> Text
-> CompressedFile
-> TCM ()
generateHTML :: TCM ()
generateHTML :: TCM ()
generateHTML = PageGen -> TCM ()
generateHTMLWithPageGen PageGen
pageGen
where
pageGen :: PageGen
pageGen :: PageGen
pageGen dir :: FilePath
dir ft :: FileType
ft pc :: Bool
pc ext :: FilePath
ext mod :: TopLevelModuleName
mod contents :: Text
contents hinfo :: CompressedFile
hinfo =
(FilePath -> FilePath -> Text)
-> FilePath -> FilePath -> TopLevelModuleName -> TCM ()
generatePage (Bool -> FileType -> FilePath -> FilePath -> Text
renderer Bool
pc FileType
ft) FilePath
ext FilePath
dir TopLevelModuleName
mod
where
renderer :: Bool -> FileType -> FilePath -> FilePath -> Text
renderer :: Bool -> FileType -> FilePath -> FilePath -> Text
renderer onlyCode :: Bool
onlyCode fileType :: FileType
fileType css :: FilePath
css _ =
FilePath -> Bool -> TopLevelModuleName -> Html -> Text
page FilePath
css Bool
onlyCode TopLevelModuleName
mod (Html -> Text) -> Html -> Text
forall a b. (a -> b) -> a -> b
$
Bool -> FileType -> [TokenInfo] -> Html
code Bool
onlyCode FileType
fileType ([TokenInfo] -> Html) -> [TokenInfo] -> Html
forall a b. (a -> b) -> a -> b
$
Text -> CompressedFile -> [TokenInfo]
tokenStream Text
contents CompressedFile
hinfo
generateHTMLWithPageGen
:: PageGen
-> TCM ()
generateHTMLWithPageGen :: PageGen -> TCM ()
generateHTMLWithPageGen generatePage :: PageGen
generatePage = do
CommandLineOptions
options <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
TCM.commandLineOptions
let dir :: FilePath
dir = CommandLineOptions -> FilePath
optHTMLDir CommandLineOptions
options
let htmlHighlight :: HtmlHighlight
htmlHighlight = CommandLineOptions -> HtmlHighlight
optHTMLHighlight CommandLineOptions
options
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True FilePath
dir
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe FilePath -> Bool) -> Maybe FilePath -> Bool
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> Maybe FilePath
optCSSFile CommandLineOptions
options) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
FilePath
cssFile <- FilePath -> IO FilePath
getDataFileName FilePath
defaultCSSFile
FilePath -> FilePath -> IO ()
copyFile FilePath
cssFile (FilePath
dir FilePath -> FilePath -> FilePath
</> FilePath
defaultCSSFile)
FilePath -> VerboseLevel -> [FilePath] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
FilePath -> VerboseLevel -> a -> m ()
TCM.reportS "html" 1
[ "" :: String
, "Warning: HTML is currently generated for ALL files which can be"
, "reached from the given module, including library files."
]
((TopLevelModuleName, ModuleInfo) -> TCM ())
-> [(TopLevelModuleName, ModuleInfo)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(n :: TopLevelModuleName
n, mi :: ModuleInfo
mi) ->
let i :: Interface
i = ModuleInfo -> Interface
TCM.miInterface ModuleInfo
mi
ft :: FileType
ft = Interface -> FileType
TCM.iFileType Interface
i in
PageGen
generatePage FilePath
dir FileType
ft
(HtmlHighlight -> FileType -> Bool
highlightOnlyCode HtmlHighlight
htmlHighlight FileType
ft)
(HtmlHighlight -> FileType -> FilePath
highlightedFileExt HtmlHighlight
htmlHighlight FileType
ft) TopLevelModuleName
n
(Interface -> Text
TCM.iSource Interface
i) (Interface -> CompressedFile
TCM.iHighlighting Interface
i)) ([(TopLevelModuleName, ModuleInfo)] -> TCM ())
-> (Map TopLevelModuleName ModuleInfo
-> [(TopLevelModuleName, ModuleInfo)])
-> Map TopLevelModuleName ModuleInfo
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Map TopLevelModuleName ModuleInfo
-> [(TopLevelModuleName, ModuleInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map TopLevelModuleName ModuleInfo -> TCM ())
-> TCMT IO (Map TopLevelModuleName ModuleInfo) -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Map TopLevelModuleName ModuleInfo)
TCM.getVisitedModules
modToFile :: C.TopLevelModuleName -> String -> FilePath
modToFile :: TopLevelModuleName -> FilePath -> FilePath
modToFile m :: TopLevelModuleName
m ext :: FilePath
ext =
FilePath -> FilePath
Network.URI.Encode.encode (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$
Doc -> FilePath
render (TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
m) FilePath -> FilePath -> FilePath
<.> FilePath
ext
generatePage
:: (FilePath -> FilePath -> Text)
-> String
-> FilePath
-> C.TopLevelModuleName
-> TCM ()
generatePage :: (FilePath -> FilePath -> Text)
-> FilePath -> FilePath -> TopLevelModuleName -> TCM ()
generatePage renderPage :: FilePath -> FilePath -> Text
renderPage ext :: FilePath
ext dir :: FilePath
dir mod :: TopLevelModuleName
mod = do
AbsolutePath
f <- AbsolutePath -> Maybe AbsolutePath -> AbsolutePath
forall a. a -> Maybe a -> a
fromMaybe AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe AbsolutePath -> AbsolutePath)
-> (Map TopLevelModuleName AbsolutePath -> Maybe AbsolutePath)
-> Map TopLevelModuleName AbsolutePath
-> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName
-> Map TopLevelModuleName AbsolutePath -> Maybe AbsolutePath
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
mod (Map TopLevelModuleName AbsolutePath -> AbsolutePath)
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
-> TCMT IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map TopLevelModuleName AbsolutePath) TCState
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
TCM.stModuleToSource
FilePath
css <- FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
defaultCSSFile (Maybe FilePath -> FilePath)
-> (CommandLineOptions -> Maybe FilePath)
-> CommandLineOptions
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> Maybe FilePath
optCSSFile (CommandLineOptions -> FilePath)
-> TCMT IO CommandLineOptions -> TCMT IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
TCM.commandLineOptions
let target :: FilePath
target = FilePath
dir FilePath -> FilePath -> FilePath
</> TopLevelModuleName -> FilePath -> FilePath
modToFile TopLevelModuleName
mod FilePath
ext
let html :: Text
html = FilePath -> FilePath -> Text
renderPage FilePath
css (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> FilePath
filePath AbsolutePath
f
FilePath -> VerboseLevel -> FilePath -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
FilePath -> VerboseLevel -> FilePath -> m ()
TCM.reportSLn "html" 1 (FilePath -> TCM ()) -> FilePath -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Generating HTML for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
Doc -> FilePath
render (TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
mod) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
" (" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
target FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")."
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Text -> IO ()
UTF8.writeTextToFile FilePath
target Text
html
(!!) :: Html -> [Attribute] -> Html
h :: Html
h !! :: Html -> [Attribute] -> Html
!! as :: [Attribute]
as = Html
h Html -> Attribute -> Html
forall h. Attributable h => h -> Attribute -> h
! [Attribute] -> Attribute
forall a. Monoid a => [a] -> a
mconcat [Attribute]
as
page :: FilePath
-> Bool
-> C.TopLevelModuleName
-> Html
-> Text
page :: FilePath -> Bool -> TopLevelModuleName -> Html -> Text
page css :: FilePath
css htmlHighlight :: Bool
htmlHighlight modName :: TopLevelModuleName
modName pageContent :: Html
pageContent =
Html -> Text
renderHtml (Html -> Text) -> Html -> Text
forall a b. (a -> b) -> a -> b
$ if Bool
htmlHighlight
then Html
pageContent
else Html -> Html
docTypeHtml (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ Html
hdr Html -> Html -> Html
forall a. Semigroup a => a -> a -> a
<> Html
rest
where
hdr :: Html
hdr = Html -> Html
Html5.head (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat
[ Html
meta Html -> [Attribute] -> Html
!! [ AttributeValue -> Attribute
charset "utf-8" ]
, Html -> Html
Html5.title (FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml (FilePath -> Html) -> FilePath -> Html
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
render (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
modName)
, Html
link Html -> [Attribute] -> Html
!! [ AttributeValue -> Attribute
rel "stylesheet"
, AttributeValue -> Attribute
href (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue FilePath
css
]
]
rest :: Html
rest = Html -> Html
body (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ (Html -> Html
pre (Html -> Html) -> Attribute -> Html -> Html
forall h. Attributable h => h -> Attribute -> h
! AttributeValue -> Attribute
class_ "Agda") Html
pageContent
type TokenInfo =
( Int
, String
, Aspects
)
tokenStream
:: Text
-> CompressedFile
-> [TokenInfo]
tokenStream :: Text -> CompressedFile -> [TokenInfo]
tokenStream contents :: Text
contents info :: CompressedFile
info =
([(Maybe Aspects, (VerboseLevel, Char))] -> TokenInfo)
-> [[(Maybe Aspects, (VerboseLevel, Char))]] -> [TokenInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\cs :: [(Maybe Aspects, (VerboseLevel, Char))]
cs -> case [(Maybe Aspects, (VerboseLevel, Char))]
cs of
(mi :: Maybe Aspects
mi, (pos :: VerboseLevel
pos, _)) : _ ->
(VerboseLevel
pos, ((Maybe Aspects, (VerboseLevel, Char)) -> Char)
-> [(Maybe Aspects, (VerboseLevel, Char))] -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map ((VerboseLevel, Char) -> Char
forall a b. (a, b) -> b
snd ((VerboseLevel, Char) -> Char)
-> ((Maybe Aspects, (VerboseLevel, Char)) -> (VerboseLevel, Char))
-> (Maybe Aspects, (VerboseLevel, Char))
-> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Aspects, (VerboseLevel, Char)) -> (VerboseLevel, Char)
forall a b. (a, b) -> b
snd) [(Maybe Aspects, (VerboseLevel, Char))]
cs, Aspects -> Maybe Aspects -> Aspects
forall a. a -> Maybe a -> a
fromMaybe Aspects
forall a. Monoid a => a
mempty Maybe Aspects
mi)
[] -> TokenInfo
forall a. HasCallStack => a
__IMPOSSIBLE__) ([[(Maybe Aspects, (VerboseLevel, Char))]] -> [TokenInfo])
-> [[(Maybe Aspects, (VerboseLevel, Char))]] -> [TokenInfo]
forall a b. (a -> b) -> a -> b
$
((Maybe Aspects, (VerboseLevel, Char))
-> (Maybe Aspects, (VerboseLevel, Char)) -> Bool)
-> [(Maybe Aspects, (VerboseLevel, Char))]
-> [[(Maybe Aspects, (VerboseLevel, Char))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (Maybe Aspects -> Maybe Aspects -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Maybe Aspects -> Maybe Aspects -> Bool)
-> ((Maybe Aspects, (VerboseLevel, Char)) -> Maybe Aspects)
-> (Maybe Aspects, (VerboseLevel, Char))
-> (Maybe Aspects, (VerboseLevel, Char))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Maybe Aspects, (VerboseLevel, Char)) -> Maybe Aspects
forall a b. (a, b) -> a
fst) ([(Maybe Aspects, (VerboseLevel, Char))]
-> [[(Maybe Aspects, (VerboseLevel, Char))]])
-> [(Maybe Aspects, (VerboseLevel, Char))]
-> [[(Maybe Aspects, (VerboseLevel, Char))]]
forall a b. (a -> b) -> a -> b
$
((VerboseLevel, Char) -> (Maybe Aspects, (VerboseLevel, Char)))
-> [(VerboseLevel, Char)]
-> [(Maybe Aspects, (VerboseLevel, Char))]
forall a b. (a -> b) -> [a] -> [b]
map (\(pos :: VerboseLevel
pos, c :: Char
c) -> (VerboseLevel -> IntMap Aspects -> Maybe Aspects
forall a. VerboseLevel -> IntMap a -> Maybe a
IntMap.lookup VerboseLevel
pos IntMap Aspects
infoMap, (VerboseLevel
pos, Char
c))) ([(VerboseLevel, Char)] -> [(Maybe Aspects, (VerboseLevel, Char))])
-> [(VerboseLevel, Char)]
-> [(Maybe Aspects, (VerboseLevel, Char))]
forall a b. (a -> b) -> a -> b
$
[VerboseLevel] -> FilePath -> [(VerboseLevel, Char)]
forall a b. [a] -> [b] -> [(a, b)]
zip [1..] (Text -> FilePath
T.unpack Text
contents)
where
infoMap :: IntMap Aspects
infoMap = File -> IntMap Aspects
toMap (CompressedFile -> File
decompress CompressedFile
info)
code :: Bool
-> FileType
-> [TokenInfo]
-> Html
code :: Bool -> FileType -> [TokenInfo] -> Html
code onlyCode :: Bool
onlyCode fileType :: FileType
fileType = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> ([TokenInfo] -> [Html]) -> [TokenInfo] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
onlyCode
then case FileType
fileType of
RstFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkRst ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
MdFileType -> ([[TokenInfo]] -> Html) -> [[[TokenInfo]]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [[TokenInfo]] -> Html
mkMd ([[[TokenInfo]]] -> [Html])
-> ([TokenInfo] -> [[[TokenInfo]]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> [[TokenInfo]] -> [[[TokenInfo]]]
forall e. VerboseLevel -> [e] -> [[e]]
chunksOf 2 ([[TokenInfo]] -> [[[TokenInfo]]])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [[[TokenInfo]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
AgdaFileType -> (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
mkHtml
TexFileType -> ([[TokenInfo]] -> Html) -> [[[TokenInfo]]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [[TokenInfo]] -> Html
mkMd ([[[TokenInfo]]] -> [Html])
-> ([TokenInfo] -> [[[TokenInfo]]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> [[TokenInfo]] -> [[[TokenInfo]]]
forall e. VerboseLevel -> [e] -> [[e]]
chunksOf 2 ([[TokenInfo]] -> [[[TokenInfo]]])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [[[TokenInfo]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
OrgFileType -> ([TokenInfo] -> Html) -> [[TokenInfo]] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map [TokenInfo] -> Html
mkOrg ([[TokenInfo]] -> [Html])
-> ([TokenInfo] -> [[TokenInfo]]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TokenInfo] -> [[TokenInfo]]
splitByMarkup
else (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
mkHtml
where
trd :: (a, b, c) -> c
trd (_, _, a :: c
a) = c
a
splitByMarkup :: [TokenInfo] -> [[TokenInfo]]
splitByMarkup :: [TokenInfo] -> [[TokenInfo]]
splitByMarkup = (TokenInfo -> Bool) -> [TokenInfo] -> [[TokenInfo]]
forall a. (a -> Bool) -> [a] -> [[a]]
splitWhen ((TokenInfo -> Bool) -> [TokenInfo] -> [[TokenInfo]])
-> (TokenInfo -> Bool) -> [TokenInfo] -> [[TokenInfo]]
forall a b. (a -> b) -> a -> b
$ (Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Markup) (Maybe Aspect -> Bool)
-> (TokenInfo -> Maybe Aspect) -> TokenInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aspects -> Maybe Aspect
aspect (Aspects -> Maybe Aspect)
-> (TokenInfo -> Aspects) -> TokenInfo -> Maybe Aspect
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TokenInfo -> Aspects
forall a b c. (a, b, c) -> c
trd
mkHtml :: TokenInfo -> Html
mkHtml :: TokenInfo -> Html
mkHtml (pos :: VerboseLevel
pos, s :: FilePath
s, mi :: Aspects
mi) =
Bool -> (Html -> Html) -> Html -> Html
forall a. Bool -> (a -> a) -> a -> a
applyUnless (Aspects
mi Aspects -> Aspects -> Bool
forall a. Eq a => a -> a -> Bool
== Aspects
forall a. Monoid a => a
mempty) (VerboseLevel -> Aspects -> Html -> Html
annotate VerboseLevel
pos Aspects
mi) (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml FilePath
s
mkRst :: [TokenInfo] -> Html
mkRst :: [TokenInfo] -> Html
mkRst = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> ([TokenInfo] -> [Html]) -> [TokenInfo] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> Html
forall a. ToMarkup a => a -> Html
toHtml FilePath
rstDelimiter Html -> [Html] -> [Html]
forall a. a -> [a] -> [a]
:) ([Html] -> [Html])
-> ([TokenInfo] -> [Html]) -> [TokenInfo] -> [Html]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
go
where
go :: TokenInfo -> Html
go token :: TokenInfo
token@(_, s :: FilePath
s, mi :: Aspects
mi) = if Aspects -> Maybe Aspect
aspect Aspects
mi Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Background
then FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
s
else TokenInfo -> Html
mkHtml TokenInfo
token
mkMd :: [[TokenInfo]] -> Html
mkMd :: [[TokenInfo]] -> Html
mkMd = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html)
-> ([[TokenInfo]] -> [Html]) -> [[TokenInfo]] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TokenInfo]] -> [Html]
go
where
work :: TokenInfo -> Html
work token :: TokenInfo
token@(_, s :: FilePath
s, mi :: Aspects
mi) = case Aspects -> Maybe Aspect
aspect Aspects
mi of
Just Background -> FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
s
Just Markup -> Html
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> TokenInfo -> Html
mkHtml TokenInfo
token
go :: [[TokenInfo]] -> [Html]
go [a :: [TokenInfo]
a, b :: [TokenInfo]
b] = [ [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$ TokenInfo -> Html
work (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
a
, Html -> Html
pre (Html -> Html) -> Attribute -> Html -> Html
forall h. Attributable h => h -> Attribute -> h
! AttributeValue -> Attribute
class_ "Agda" (Html -> Html) -> Html -> Html
forall a b. (a -> b) -> a -> b
$ [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$ TokenInfo -> Html
work (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
b
]
go [a :: [TokenInfo]
a] = TokenInfo -> Html
work (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TokenInfo]
a
go _ = [Html]
forall a. HasCallStack => a
__IMPOSSIBLE__
mkOrg :: [TokenInfo] -> Html
mkOrg :: [TokenInfo] -> Html
mkOrg = [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> ([TokenInfo] -> [Html]) -> [TokenInfo] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TokenInfo -> Html) -> [TokenInfo] -> [Html]
forall a b. (a -> b) -> [a] -> [b]
map TokenInfo -> Html
go
where
go :: TokenInfo -> Html
go token :: TokenInfo
token@(_, s :: FilePath
s, mi :: Aspects
mi) = if Aspects -> Maybe Aspect
aspect Aspects
mi Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Background
then FilePath -> Html
forall a. ToMarkup a => a -> Html
preEscapedToHtml FilePath
s
else TokenInfo -> Html
mkHtml TokenInfo
token
annotate :: Int -> Aspects -> Html -> Html
annotate :: VerboseLevel -> Aspects -> Html -> Html
annotate pos :: VerboseLevel
pos mi :: Aspects
mi = Bool -> (Html -> Html) -> Html -> Html
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
hereAnchor
([Attribute] -> Html -> Html
anchorage [Attribute]
nameAttributes Html
forall a. Monoid a => a
mempty Html -> Html -> Html
forall a. Semigroup a => a -> a -> a
<>) (Html -> Html) -> (Html -> Html) -> Html -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Attribute] -> Html -> Html
anchorage [Attribute]
posAttributes
where
anchorage :: [Attribute] -> Html -> Html
anchorage :: [Attribute] -> Html -> Html
anchorage attrs :: [Attribute]
attrs html :: Html
html = Html -> Html
a Html
html Html -> [Attribute] -> Html
!! [Attribute]
attrs
posAttributes :: [Attribute]
posAttributes :: [Attribute]
posAttributes = [[Attribute]] -> [Attribute]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [AttributeValue -> Attribute
Attr.id (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> FilePath
forall a. Show a => a -> FilePath
show VerboseLevel
pos ]
, Maybe Attribute -> [Attribute]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Maybe Attribute -> [Attribute]) -> Maybe Attribute -> [Attribute]
forall a b. (a -> b) -> a -> b
$ (DefinitionSite -> Attribute)
-> Maybe DefinitionSite -> Maybe Attribute
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefinitionSite -> Attribute
link (Maybe DefinitionSite -> Maybe Attribute)
-> Maybe DefinitionSite -> Maybe Attribute
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi
, AttributeValue -> Attribute
class_ (FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath]
classes) Attribute -> [()] -> [Attribute]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
classes)
]
nameAttributes :: [Attribute]
nameAttributes :: [Attribute]
nameAttributes = [ AttributeValue -> Attribute
Attr.id (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Maybe FilePath
mDefSiteAnchor ]
classes :: [FilePath]
classes = [[FilePath]] -> [FilePath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ (FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FilePath -> [FilePath]
forall p a. p -> [a]
noteClasses (Aspects -> Maybe FilePath
note Aspects
mi)
, [OtherAspect] -> [FilePath]
otherAspectClasses (Set OtherAspect -> [OtherAspect]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Set OtherAspect -> [OtherAspect])
-> Set OtherAspect -> [OtherAspect]
forall a b. (a -> b) -> a -> b
$ Aspects -> Set OtherAspect
otherAspects Aspects
mi)
, (Aspect -> [FilePath]) -> Maybe Aspect -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Aspect -> [FilePath]
aspectClasses (Aspects -> Maybe Aspect
aspect Aspects
mi)
]
aspectClasses :: Aspect -> [FilePath]
aspectClasses (Name mKind :: Maybe NameKind
mKind op :: Bool
op) = [FilePath]
kindClass [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
opClass
where
kindClass :: [FilePath]
kindClass = Maybe FilePath -> [FilePath]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Maybe FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (NameKind -> FilePath) -> Maybe NameKind -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NameKind -> FilePath
showKind Maybe NameKind
mKind
showKind :: NameKind -> FilePath
showKind (Constructor Inductive) = "InductiveConstructor"
showKind (Constructor CoInductive) = "CoinductiveConstructor"
showKind k :: NameKind
k = NameKind -> FilePath
forall a. Show a => a -> FilePath
show NameKind
k
opClass :: [FilePath]
opClass = if Bool
op then ["Operator"] else []
aspectClasses a :: Aspect
a = [Aspect -> FilePath
forall a. Show a => a -> FilePath
show Aspect
a]
otherAspectClasses :: [OtherAspect] -> [FilePath]
otherAspectClasses = (OtherAspect -> FilePath) -> [OtherAspect] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> FilePath
forall a. Show a => a -> FilePath
show
noteClasses :: p -> [a]
noteClasses s :: p
s = []
hereAnchor :: Bool
hereAnchor :: Bool
hereAnchor = Bool
here Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
mDefSiteAnchor
mDefinitionSite :: Maybe DefinitionSite
mDefinitionSite :: Maybe DefinitionSite
mDefinitionSite = Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi
here :: Bool
here :: Bool
here = Bool -> (DefinitionSite -> Bool) -> Maybe DefinitionSite -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False DefinitionSite -> Bool
defSiteHere Maybe DefinitionSite
mDefinitionSite
mDefSiteAnchor :: Maybe String
mDefSiteAnchor :: Maybe FilePath
mDefSiteAnchor = Maybe FilePath
-> (DefinitionSite -> Maybe FilePath)
-> Maybe DefinitionSite
-> Maybe FilePath
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe FilePath
forall a. HasCallStack => a
__IMPOSSIBLE__ DefinitionSite -> Maybe FilePath
defSiteAnchor Maybe DefinitionSite
mDefinitionSite
link :: DefinitionSite -> Attribute
link (DefinitionSite m :: TopLevelModuleName
m pos :: VerboseLevel
pos _here :: Bool
_here _aName :: Maybe FilePath
_aName) = AttributeValue -> Attribute
href (AttributeValue -> Attribute) -> AttributeValue -> Attribute
forall a b. (a -> b) -> a -> b
$ FilePath -> AttributeValue
stringValue (FilePath -> AttributeValue) -> FilePath -> AttributeValue
forall a b. (a -> b) -> a -> b
$
Bool -> (FilePath -> FilePath) -> FilePath -> FilePath
forall a. Bool -> (a -> a) -> a -> a
applyUnless (VerboseLevel
pos VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= 1)
(FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "#" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath -> FilePath
Network.URI.Encode.encode (VerboseLevel -> FilePath
forall a. Show a => a -> FilePath
show VerboseLevel
pos))
(FilePath -> FilePath
Network.URI.Encode.encode (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FilePath -> FilePath
modToFile TopLevelModuleName
m "html")