{-# LANGUAGE CPP #-} -- | Function for generating highlighted, hyperlinked HTML from Agda -- sources. module Agda.Interaction.Highlighting.PandocHTML ( 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 qualified Data.Char as Char import Text.Pandoc.Definition import qualified Text.Pandoc.Definition as Pandoc import Text.Pandoc.Options import Text.Pandoc.Readers.Markdown import Text.Pandoc.Writers.HTML import Paths_PandocAgda 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 qualified Agda.Interaction.PandocOptions as PO import Agda.Utils.FileName (filePath) import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.Pretty import Agda.Utils.Impossible #include "../../undefined.h" -- | The name of the default CSS file. defaultCSSFile :: FilePath defaultCSSFile = "Agda.css" -- | The name of the default template file for pandoc. defaultTemplateFile :: FilePath defaultTemplateFile = "Agda.template" -- | Generates HTML files from all the sources which the given module -- depends on (including the module itself). -- -- This function should only be called after type checking has -- completed successfully. generateHTML :: PO.CommandLineOptions -> A.ModuleName -> TCM () generateHTML fullopts mod = do options <- TCM.commandLineOptions -- There is a default directory given by 'defaultHTMLDir' let dir = optHTMLDir options liftIO $ createDirectoryIfMissing True dir -- If the default CSS file should be used, then it is copied to -- the output directory. 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." ] -- Pull highlighting info from the state and generate all the -- web pages. mapM_ (\(m, h) -> generatePage fullopts dir m h) =<< map (id *** TCM.iHighlighting . TCM.miInterface) . Map.toList <$> TCM.getVisitedModules -- | Converts module names to the corresponding HTML file names. modToFile :: C.TopLevelModuleName -> FilePath modToFile m = render (pretty m) <.> "html" -- | Generates an HTML file with a highlighted, hyperlinked version of -- the given module. generatePage :: PO.CommandLineOptions -> FilePath -- ^ Directory in which to create files. -> C.TopLevelModuleName -- ^ Module to be highlighted. -> HighlightingInfo -- ^ Syntax highlighting info for the module. -> TCM () generatePage fullopts 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 mSlideVariant = fmap read $ PO.optGenerateHTML fullopts html <- case mSlideVariant of Just slideVariant | isLiterate (filePath f) -> do templateFile <- maybe (liftIO $ getDataFileName defaultTemplateFile) return (PO.optTemplateFile fullopts) template <- liftIO $ UTF8.readTextFile templateFile return $ pandocPage template css slideVariant mod contents highlighting _ -> do return $ renderHtml $ page css mod contents highlighting TCM.reportSLn "html" 1 $ "Generating HTML for " ++ render (pretty mod) ++ " (" ++ target ++ ")." liftIO $ UTF8.writeFile target html where target = dir modToFile mod -- | Constructs the web page, including headers. page :: FilePath -- ^ URL to the CSS file. -> C.TopLevelModuleName -- ^ Module to be highlighted. -> String -- ^ The contents of the module. -> CompressedFile -- ^ Highlighting information. -> 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 --- | Constructs the HTML displaying the code. code :: String -- ^ The contents of the module. -> CompressedFile -- ^ Highlighting information. -> Html code contents info = mconcat $ map (\(pos, s, mi) -> annotate pos mi (stringToHtml s)) $ tokenStream contents info -- | Constructs the web page, including headers, with pandoc. pandocPage :: String -- ^ Template -> FilePath -- ^ URL to the CSS file. -> HTMLSlideVariant -- ^ Slide variant -> C.TopLevelModuleName -- ^ Module to be highlighted. -> String -- ^ The contents of the module. -> CompressedFile -- ^ Highlighting information. -> String pandocPage template css slideVariant modName contents info = writeHtmlString def { writerStandalone = True , writerTemplate = template , writerTableOfContents = True , writerSlideVariant = slideVariant , writerVariables = [("css",css)] } $ Pandoc meta $ concat $ zipWith ($) (removeCodeBlocks md []) cf where cf = (++ [[]]) . map conv . getCode . splitComment "\n\\begin{code}" . splitComment "\n\\end{code}" $ tokenStream contents info (Pandoc meta md) = readMarkdown def contents conv x = [Para [ RawInline "html" . renderHtmlFragment . (pre <<) . mconcat . map (\(pos, s, mi) -> annotate pos mi (stringToHtml s)) $ x ]] getCode ((_,s,_):xs) | s == "\n\\begin{code}" || List.isPrefixOf "\\begin{code}" s = getCode' xs [] getCode (_:xs) = getCode xs getCode [] = [] getCode' ((_,s,_):xs) | s == "\n\\end{code}" || List.isPrefixOf "\\end{code}" s = (: getCode xs) . reverse getCode' (x:xs) = getCode' xs . (x:) getCode' [] = error "__IMPOSSIBLE__" -- ??? splitComment w = concatMap f where f (pos, s, mi) = [(pos, t, mi) | t <- filter (not . null) $ g s []] g s | List.isPrefixOf w s = (: (w : g (drop (length w) s) [])) . reverse g [] = (:[]) . reverse g (c:cs) = g cs . (c:) removeCodeBlocks (RawBlock "latex" s: xs) | List.isPrefixOf "\\begin{code}" s = removeCodeBlocks' (++) xs removeCodeBlocks (RawBlock "html" s: xs) | List.isPrefixOf "