module Agda.Interaction.Highlighting.HTML
( generateHTML
, defaultCSSFile
, generateHTMLWithPageGen
, generatePage
, page
, tokenStream
, code
) where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
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.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 = generateHTMLWithPageGen pageGen
where
pageGen dir mod hinfo = generatePage renderer dir mod
where
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_ (\(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 -> FilePath -> String -> String)
-> FilePath
-> C.TopLevelModuleName
-> TCM ()
generatePage renderpage dir mod = 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 = renderpage css (filePath f) contents
TCM.reportSLn "html" 1 $ "Generating HTML for " ++
render (pretty mod) ++
" (" ++ target ++ ")."
liftIO $ UTF8.writeFile target html
where target = dir </> modToFile mod
page :: FilePath
-> C.TopLevelModuleName
-> Html
-> String
page css modName pagecontent = renderHtml $
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 << pagecontent
tokenStream
:: String
-> CompressedFile
-> [(Int, String, Aspects)]
tokenStream contents info =
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)
code :: [(Int, String, Aspects)]
-> Html
code = mconcat . map (\(pos, s, mi) -> annotate pos mi (stringToHtml s))
where
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]