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 2 years ago
example hotfix: pre → span 3 years ago
src look for references in divs 2 years ago
.gitignore Allow control of span linking 3 years ago
LICENSE first commit 3 years ago
README.md Allow control of span linking 3 years ago
Setup.hs first commit 3 years ago
agda-reference-filter.cabal first commit 3 years ago
hie.yaml first commit 3 years ago
stack.yaml first commit 3 years ago
stack.yaml.lock first commit 3 years 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.