Enables the idiom <!-- ```agda _ = X ``` --> for tricking the filter into picking the right name.
|1 week ago|
|example||1 week ago|
|src||1 week ago|
|.gitignore||1 week ago|
|LICENSE||1 week ago|
|README.md||1 week ago|
|Setup.hs||1 week ago|
|agda-reference-filter.cabal||1 week ago|
|hie.yaml||1 week ago|
|stack.yaml||1 week ago|
|stack.yaml.lock||1 week 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` 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:
If you want a span to have the
agda class but for it not to be linked,
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.