Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Function for generating highlighted, hyperlinked HTML from Agda sources.



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 #


:: (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.

generatePage Source #


:: (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.

page Source #


:: FilePath

URL to the CSS file.

-> TopLevelModuleName

Module to be highlighted.

-> Html 
-> String 

Constructs the web page, including headers.

tokenStream Source #


:: String

The contents of the module.

-> CompressedFile

Highlighting information.

-> [(Int, String, Aspects)]

(position, contents, info)

Constructs token stream ready to print.

code :: [(Int, String, Aspects)] -> Html Source #

Constructs the HTML displaying the code.