|
|
- # 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.
|