| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Highlighting.HTML
Description
Function for generating highlighted, hyperlinked HTML from Agda sources.
Synopsis
- generateHTML :: TCM ()
- defaultCSSFile :: FilePath
- generateHTMLWithPageGen :: PageGen -> TCM ()
- generatePage :: (FilePath -> FilePath -> Text) -> String -> FilePath -> TopLevelModuleName -> TCM ()
- page :: FilePath -> Bool -> TopLevelModuleName -> Html -> Text
- tokenStream :: Text -> CompressedFile -> [TokenInfo]
- code :: Bool -> FileType -> [TokenInfo] -> Html
Documentation
generateHTML :: TCM () Source #
defaultCSSFile :: FilePath Source #
The name of the default CSS file.
generateHTMLWithPageGen Source #
Arguments
| :: PageGen | Page generator. |
| -> TCM () |
Prepare information for HTML page generation.
The page generator receives the output directory as well as the module's top level module name, its source code, and its highlighting information.
Arguments
| :: (FilePath -> FilePath -> Text) | Page renderer. |
| -> String | Output file extension. |
| -> FilePath | Directory in which to create files. |
| -> TopLevelModuleName | Module to be highlighted. |
| -> TCM () |
Generates a highlighted, hyperlinked version of the given module.
Arguments
| :: FilePath | URL to the CSS file. |
| -> Bool | Whether to reserve literate |
| -> TopLevelModuleName | Module to be highlighted. |
| -> Html | |
| -> Text |
Constructs the web page, including headers.
Arguments
| :: Text | The contents of the module. |
| -> CompressedFile | Highlighting information. |
| -> [TokenInfo] |
Constructs token stream ready to print.