Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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.

generatePage Source #

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.

page Source #

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.

tokenStream Source #

Arguments

:: Text | The contents of the module.
-> CompressedFile | Highlighting information.
-> [TokenInfo] |

Constructs token stream ready to print.

code Source #

Arguments

:: Bool | Whether to generate non-code contents as-is
-> FileType | Source file type
-> [TokenInfo] |
-> Html |

Constructs the HTML displaying the code.