Idris2
Idris2 copied to clipboard
idris-lang
Add source link for individual declaration on documentation
- [x] I have read CONTRIBUTING.md.
- [x] I have checked that there is no existing PR/issue about my proposal.
Summary
Add source link for each declaration like Hackage.
Motivation
| Hackage | [Idris2] |
|---|---|
As a beginner, one of the pain point of learning Idris2 (compared to Haskell) was that I had to either clone the repo or search thru github to find out how a function works.
The proposal
For each definitions, also add source link on the right (like how Hackage does).
Technical implementation
As it is already possible to link to specific source lines like https://test.idris-lang.org/Idris2/base/source/Data.List.html#line11-line15,
Alternatives considered
kotlin documentation provides multiple link to source definition. Maybe we could provide two links, one pointing to source hosted on test.idris-lang, and the other github as well:
Conclusion
This will make documentation more approachable.
The main problem here is that docs generation is part of idris2 but
source highlighting is done using katla
When we generate the docs we cannot assume that a highlighted source
file is available. We do get the big (source) on the top RHS (visible on
your screenshot) on the official server through a bit of sed magic.
But doing so for each and every definition would be a lot harder.
would it be possible for idris2 to also include filename and line range in metadata when generating documentation? then katla could figure out which code to highlight such as {FILENAME}.html#line{A}-line{B}
Katla does not touch the docs at all, it only generates the highlighted sources.
Even though what I am about to say is a step in another direction, it still might be useful to you:
Idris2 LSP has jump-to-definition functionality which lets you hover over arbitrary top-level definition name in your type-checked source code and jump to its source. It works for definitions local to your project and definitions that reside in libraries.
