Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Highlighting.HTML

Description

Function for generating highlighted, hyperlinked HTML from Agda sources.

Synopsis

Documentation

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.