Generating HTML¶
To generate highlighted, hyperlinked web pages from source code, run the following command in a shell:
$ agda --html --html-dir={output directory} {root module}
You can change the way in which the code is highlighted by providing
your own CSS file instead of the default, included one
(use the --css
option).
Note
The Agda.css
shipped with Agda is located at
${Agda_datadir}/html/Agda.css
. Since version 2.6.2, the
Agda data directory can be printed using the option
--print-agda-dir
, which has been an alias of
--print-agda-data-dir
since 2.6.4.1.
Thus, you can get hold of the CSS file via cat $(agda
--print-agda-data-dir)/html/Agda.css
.
You can also get highlighting for all occurrences of the symbol the mouse pointer is
hovering over in the HTML by adding the --highlight-occurrences
option.
The default behaviour is to only highlight the single symbol under the mouse pointer.
If you’re using Literate Agda with Markdown or reStructedText and you
want to highlight your Agda codes with Agda’s HTML backend and render
the rest of the content (let’s call it “literate” part for convenience)
with some another renderer, you can use the --html-highlight=code
option, which makes the Agda compiler:
not wrapping the literate part into
<a class="Background">
tagsnot wrapping the generated document with a
<html>
tag, which means you’ll have to specify the CSS location somewhere else, like<link rel="stylesheet" type="text/css" href="Agda.css">
converting
<a class="Markup">
tags into<pre class="agda-code">
tags that wrap the complete Agda code block belowgenerating files with extension as-is (i.e. .lagda.md becomes .md, .lagda.rst becomes .rst)
for reStructuredText, a
.. raw:: html
will be inserted before every code blocks
This will affect all the files involved in one compilation, making
pure Agda code files rendered without HTML footer/header as well.
To use code
with literate Agda files and all
with pure Agda
files, use --html-highlight=auto
, which means auto-detection.
Options¶
--html-dir={DIR}
Changes the directory where the output is placed to
DIR
. Default:html
.--css={URL}
The CSS file used by the HTML files (
URL
can be relative).--html-highlight=[code,all,auto]
Highlight Agda code only or everything in the generated HTML files. Default:
all
.