| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Interaction.Highlighting.HTML
Description
Function for generating highlighted, hyperlinked HTML from Agda sources.
- generateHTML :: TCM ()
- defaultCSSFile :: FilePath
- generateHTMLWithPageGen :: (FilePath -> TopLevelModuleName -> CompressedFile -> TCM ()) -> TCM ()
- generatePage :: (FilePath -> FilePath -> String -> String) -> FilePath -> TopLevelModuleName -> TCM ()
- page :: FilePath -> TopLevelModuleName -> Html -> String
- tokenStream :: String -> CompressedFile -> [(Int, String, Aspects)]
- code :: [(Int, String, Aspects)] -> Html
Documentation
generateHTML :: TCM () Source
Generates HTML files from all the sources which have been visited during the type checking phase.
This function should only be called after type checking has completed successfully.
defaultCSSFile :: FilePath Source
The name of the default CSS file.
generateHTMLWithPageGen Source
Arguments
| :: (FilePath -> TopLevelModuleName -> CompressedFile -> TCM ()) | Page generator |
| -> TCM () |
Prepare information for HTML page generation.
The page generator receives the file path of the module, the top level module name of the module and the highlighting information of the module.
Arguments
| :: (FilePath -> FilePath -> String -> String) | Page renderer |
| -> 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. |
| -> TopLevelModuleName | Module to be highlighted. |
| -> Html | |
| -> String |
Constructs the web page, including headers.
Arguments
| :: String | The contents of the module. |
| -> CompressedFile | Highlighting information. |
| -> [(Int, String, Aspects)] | (position, contents, info) |
Constructs token stream ready to print.