This library provides a very simple function that translates just the code blocks of a literate Agda file to colourised, hyperlinked HTML. The output of this can then be run through Pandoc or other document processors to allow literate Agda to be comfortably written in any format that allows inline HTML snippets.

There is also a simple command-line application (agda-snippets) included that can be used as a standalone file processor.

The location of library source hyperlinks is configurable, as is the CSS class given to Agda code blocks.

Usually, I try to keep the development version of this library working with the development version of Agda. This is not always 100% reliable, as I only update the library when I update my Agda installation. It will always work with the latest stable version of Agda.

Stable releases of this library are published on Hackage, as per usual, and these releases are fixed to particular Agda versions. The version of the library matches the exact Agda version it corresponds to, and thus it doesn’t follow the PVP.

To see what the output looks like, you can look at this article on my blog, which makes use of this library to render the Agda snippets.

You can install this library and the document processing tool from Hackage using stack:

stack install agda-snippets

or using Cabal:

cabal install agda-snippets

If you want to use the development version from this repository, you will have to have the correct version of Agda already available. The simplest way to do this is to edit stack.yaml, to point to the location of your Agda repository, and use stack to build the library.

The executable agda-snippets, once installed, can be invoked according to the following schema:

agda-snippets input-file.lagda output-file css-class-name /lib/uri/ [agda options] 

If you’re using stack, you may wish to invoke a local copy using stack exec:

stack exec agda-snippets -- input-file.lagda output-file css-class-name /lib/uri/ [agda options] 

The arguments are as follows:

• input-file.lagda - The Literate Agda file to process.
• output-file - Where to write the output text, where code blocks are replaced with HTML.
• css-class-name - The name of the CSS class to assign to Agda code blocks.
• /lib/uri/ - The base URI where Agda library listings are located. This is for hyperlinks for sources imported from (e.g) the Agda standard library.
• [agda options] - Any additional options are passed directly into Agda.

The library interface consists of a single function, renderAgdaSnippets, which has an interface more or less exactly like the executable above.

See the Haddocks in the Hackage listing for more details.

Some parts of this code were based on a few snippets written by Daniel Peebles a long time ago. Not sure how much of it is still his code, but thanks are due to him.