search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

feat: Add support for `vscode://file/` source links #171

Closed joehendrix closed 8 months ago

joehendrix commented 8 months ago

This makes some changes to source code url resolution to allow vscode://file/ urls. I find this useful for quickly jumping to the source code when browsing locally generated documentation.

This changes the default is to use VSCode urls if the git repo has changed. This may not be the right approach. We could further generalize how resolution occurs, but I thought I'd submit the PR and start a discussion.

hargoniX commented 8 months ago

How about checking the EDITOR environment variable? If it is either not set or has a value that is not code we use file:// and otherwise the vscode:// URIs. That way we can also add support for other editor URIs in the future rather easily.

joehendrix commented 8 months ago

I thought about this a bit more, and decided overloading EDITOR may be a little confusing. Instead, I added an explicit DOCGEN_SRC variable. Leaving it unset preserves the original behavior.

I expect most users don't generate local documentation, but I think it's useful for reviewing documentation and then quickly jumping to source for improving it.