Amélia Liao 082b5576e7 | 2 years ago | |
---|---|---|
example | 3 years ago | |
src | 2 years ago | |
.gitignore | 3 years ago | |
LICENSE | 3 years ago | |
README.md | 3 years ago | |
Setup.hs | 3 years ago | |
agda-reference-filter.cabal | 3 years ago | |
hie.yaml | 3 years ago | |
stack.yaml | 3 years ago | |
stack.yaml.lock | 3 years ago |
A Pandoc filter for linking Agda identifiers in inline code blocks.
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.
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.
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.