module Agda.Interaction.Highlighting.HTML
( generateHTML
) where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import Control.Monad.State.Class
import Control.Arrow ((***))
import System.FilePath
import System.Directory
import Text.XHtml.Strict
import Data.Function
import Data.Monoid
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.List as List
import Paths_Agda
import Agda.Interaction.FindFile
import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Highlighting.Precise
import Agda.Interaction.Highlighting.Range
import Agda.TypeChecking.Monad (TCM)
import qualified Agda.TypeChecking.Monad as TCM
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Common
import qualified Agda.Syntax.Scope.Monad as Scope
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Interaction.Options
import Agda.Utils.FileName (filePath)
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Pretty
import Agda.Utils.Impossible
#include "../../undefined.h"
defaultCSSFile :: FilePath
defaultCSSFile = "Agda.css"
generateHTML :: A.ModuleName -> TCM ()
generateHTML mod = 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 (id *** 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 . TCM.stModuleToSource <$> get
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) -> (Map.lookup pos infoMap, (pos, c))) $
zip [1..] contents
where
infoMap = toMap (decompress info)
annotate :: Integer -> MetaInfo -> 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]