{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
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.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.Text.Lazy (Text)
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.Highlighting.Precise
import Agda.Interaction.Options
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)
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"
generateHTML :: TCM ()
generateHTML = generateHTMLWithPageGen pageGen
where
pageGen :: FilePath -> C.TopLevelModuleName -> CompressedFile -> TCM ()
pageGen dir mod hinfo = generatePage renderer dir mod
where
renderer :: FilePath -> FilePath -> String -> Text
renderer css _ contents = page css mod $ code $ tokenStream contents hinfo
generateHTMLWithPageGen
:: (FilePath -> C.TopLevelModuleName -> CompressedFile -> TCM ())
-> TCM ()
generateHTMLWithPageGen generatePage = do
options <- TCM.commandLineOptions
let dir = optHTMLDir 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_ (uncurry $ generatePage dir) =<<
map (mapSnd $ TCM.iHighlighting . TCM.miInterface) .
Map.toList <$> TCM.getVisitedModules
modToFile :: C.TopLevelModuleName -> FilePath
modToFile m =
Network.URI.Encode.encode $
render (pretty m) <.> "html"
generatePage
:: (FilePath -> FilePath -> String -> Text)
-> FilePath
-> C.TopLevelModuleName
-> TCM ()
generatePage renderpage dir mod = do
f <- fromMaybe __IMPOSSIBLE__ . Map.lookup mod <$> use TCM.stModuleToSource
contents <- liftIO $ UTF8.readTextFile $ filePath f
css <- fromMaybe defaultCSSFile . optCSSFile <$>
TCM.commandLineOptions
let html = renderpage css (filePath f) contents
TCM.reportSLn "html" 1 $ "Generating HTML for " ++
render (pretty mod) ++
" (" ++ target ++ ")."
liftIO $ UTF8.writeTextToFile target html
where target = dir </> modToFile mod
(!!) :: Html -> [Attribute] -> Html
h !! as = h ! mconcat as
page :: FilePath
-> C.TopLevelModuleName
-> Html
-> Text
page css modName pagecontent = renderHtml $ 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 pagecontent)
tokenStream
:: String
-> CompressedFile
-> [(Int, String, Aspects)]
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..] contents
where
infoMap = toMap (decompress info)
code :: [(Int, String, Aspects)]
-> Html
code = mconcat . map mkHtml
where
mkHtml :: (Int, String, Aspects) -> Html
mkHtml (pos, s, mi) =
applyUnless (mi == mempty) (annotate pos mi) $ toHtml s
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 (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)