Filter for linking Agda identifiers in inline code spans
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
Amélia Liao 082b5576e7 look for references in divs 8 months ago
example hotfix: pre → span 10 months ago
src look for references in divs 8 months ago
.gitignore Allow control of span linking 10 months ago
LICENSE first commit 10 months ago
README.md Allow control of span linking 10 months ago
Setup.hs first commit 10 months ago
agda-reference-filter.cabal first commit 10 months ago
hie.yaml first commit 10 months ago
stack.yaml first commit 10 months ago
stack.yaml.lock first commit 10 months ago

README.md

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:

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.