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