# agda-reference-filter

A Pandoc filter for linking Agda identifiers in inline code blocks.

## Usage

The filter operates on Markdown files generated by Agda's built-in
literate programming support (use `--html-highlight=auto` to keep the
Markdown), then call Pandoc with the filter:

```bash
agda --html-highlight=auto --html example.lagda.md
pandoc --filter agda-reference-filter -i example.md -o example.html
```

The input file will be scanned, in source order, to build a variable
name - HTML element association.

Only the first reference is counted: if you have two identifiers called
`go`, then `` `go` `` in Markdown will link to the first.

### Controlling whether spans are linked

Code spans in Markdown are only linked if they have the `agda` - **case
insensitive** - class. In Pandoc syntax, you can attach a class to a
code span like so:

```
`List`{.agda}
```

If you want a span to have the `agda` class but for it not to be linked,
add the `nolink` class.

### Controlling what spans are linked to

If a span has the `ident` attribute, then the value of that attribute
will be used as the identifier to link to instead of the span text.