module Agda.Interaction.Highlighting.HTML
( generateHTML
) where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import Control.Monad.State.Class
import Data.Function
import Data.Monoid
import Data.Maybe
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import qualified Data.List as List
import System.FilePath
import System.Directory
import Text.XHtml.Strict
import Paths_Agda
import Agda.Interaction.Highlighting.Precise
import Agda.Interaction.Options
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Common
import Agda.TypeChecking.Monad (TCM)
import qualified Agda.TypeChecking.Monad as TCM
import Agda.Utils.FileName (filePath)
import Agda.Utils.Lens
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Pretty
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
defaultCSSFile :: FilePath
defaultCSSFile = "Agda.css"
generateHTML :: TCM ()
generateHTML = 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_ (\(m, h) -> generatePage dir m h) =<<
map (mapSnd $ TCM.iHighlighting . TCM.miInterface) .
Map.toList <$> TCM.getVisitedModules
modToFile :: C.TopLevelModuleName -> FilePath
modToFile m = render (pretty m) <.> "html"
generatePage
:: FilePath
-> C.TopLevelModuleName
-> HighlightingInfo
-> TCM ()
generatePage dir mod highlighting = do
mf <- Map.lookup mod <$> use TCM.stModuleToSource
case mf of
Nothing -> __IMPOSSIBLE__
Just f -> do
contents <- liftIO $ UTF8.readTextFile $ filePath f
css <- maybe defaultCSSFile id . optCSSFile <$>
TCM.commandLineOptions
let html = page css mod contents highlighting
TCM.reportSLn "html" 1 $ "Generating HTML for " ++
render (pretty mod) ++
" (" ++ target ++ ")."
liftIO $ UTF8.writeFile target (renderHtml html)
where target = dir </> modToFile mod
page :: FilePath
-> C.TopLevelModuleName
-> String
-> CompressedFile
-> Html
page css modName contents info =
header (thetitle << render (pretty modName)
+++
meta ! [ httpequiv "Content-Type"
, content "text/html; charset=UTF-8"
]
+++
meta ! [ httpequiv "Content-Style-Type"
, content "text/css"
]
+++
thelink noHtml ! [ href css
, rel "stylesheet"
, thetype "text/css"
])
+++
body << pre << code contents info
code :: String
-> CompressedFile
-> Html
code contents info =
mconcat $
map (\(pos, s, mi) -> annotate pos mi (stringToHtml s)) $
map (\cs -> case cs of
(mi, (pos, _)) : _ ->
(pos, map (snd . snd) cs, maybe mempty id mi)
[] -> __IMPOSSIBLE__) $
List.groupBy ((==) `on` fst) $
map (\(pos, c) -> (IntMap.lookup pos infoMap, (pos, c))) $
zip [1..] contents
where
infoMap = toMap (decompress info)
annotate :: Int -> Aspects -> Html -> Html
annotate pos mi = anchor ! attributes
where
attributes =
[name (show pos)] ++
maybe [] link (definitionSite mi) ++
(case classes of
[] -> []
cs -> [theclass $ unwords cs])
classes =
maybe [] noteClasses (note mi)
++ otherAspectClasses (otherAspects mi)
++ maybe [] aspectClasses (aspect mi)
aspectClasses (Name mKind op) = kindClass ++ opClass
where
kindClass = maybe [] ((: []) . 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 = []
link (m, pos) = [href $ modToFile m ++ "#" ++ show pos]