[ feat ] Add source location metadata to generated HTML docs

[cypheon]

Description

Attach FC info to HTML docs via data-* attributes, to allow an external tool to jump from documentation to the exact line in the (annotated) source file.

Concept

My idea was to decouple as much as possible the documentation generation (core feature of Idris2) from any external (future) docs viewer applications and source-to-HTML converters (e.g. katla) that have broader scope.

Since the Idris2 compiler does not know where (and if) the source files will be placed relatively to the HTML files, it is not feasible to emit full links. The flag --install-with-src copies the source, but it's the plain source, not a format that allows jumping to a specific line.

An external docs viewer knows if and where it can find the HTML-converted source files for a given package. It just needs the raw info: what the source filename is (represented by the module info) and where (most importantly which line) in that file a given identifier is declared.

Proposed solution

The FC metadata is added as presentation-neutral attributes data-src-mod and data-src-start to track an identifier's originating module name and source file context, respectively.

This additional information can be used by an external tool which has both the docs and the (annotated) source files available to attach links to the exact source position for each identifier. The linking can either be done with a post-processing step on the HTML files, or via injected JS, that's up to whatever tool is handling the linking.

Self-check

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md
• I confirm that this contribution did not involve GenerativeAI nor Large Language Models.