feat(dhall-docs): Jump on URLs expressions

[german1608]

Context

This is the first PR for the jump-to-definition feature. It took more time than I expected but it's working properly and the code can be enhanced to follow up next jump-to-definition elements.

Solution

The current "render source code" function used the Dhall.Pretty module's function to render the code as HTML with syntax-highlighting. Sadly, that approach wouldn't allow us to inject more properties since after an Expr Src a is transformed into a SimpleDocStream Ann we lose all information about the syntactic elements.

This new approach takes the (Src, Import)s from the source code consuming the file contents, injecting the anchors where it's needed. I took some inspiration from the dhall-lsp-server's embedWithRanges function to do this.

As a consequence, we will need to code again the syntax-highlighting algorithm but that can be done after finishing the difficult features as jump-to-definition and type-on-hover.

I did split the code a little bit to keep the source code rendering logic in a separate module to keep it more organized, but probably the next features will need even more code moving. So If you don't like the current one it doesn't matter: it will probably change. At the end of the project, we can do a global cleanup.

EDIT: I forgot to mention, but assertions and types on index are rendered by formatting the code in a single line using dhall format, parsing the result (again, to regenereate SourcePos's) and finally passing the result to the renderer function

[german1608]

I have to mention that the amount of value by adding this feature can be noted by checking the new generated Prelude documentation with the links on each package.dhall file

[sjakobi]

@german1608 So the links in https://hydra.dhall-lang.org/build/68167/download/1/2845008dce928763f4aefa94ee71d0042325f05c463272339150499eab3a20aa-Prelude/package.dhall.html are an example of this work, right?

Note that the links in e.g. https://hydra.dhall-lang.org/build/68167/download/1/2845008dce928763f4aefa94ee71d0042325f05c463272339150499eab3a20aa-Prelude/Bool/package.dhall.html give 404s.

[german1608]

@german1608 So the links in https://hydra.dhall-lang.org/build/68167/download/1/2845008dce928763f4aefa94ee71d0042325f05c463272339150499eab3a20aa-Prelude/package.dhall.html are an example of this work, right?

Note that the links in e.g. https://hydra.dhall-lang.org/build/68167/download/1/2845008dce928763f4aefa94ee71d0042325f05c463272339150499eab3a20aa-Prelude/Bool/package.dhall.html give 404s.

Yes, those are the links. I'm aware they give 404 because we don't generate docs for files without .dhall extension. A solution would be to update the imports on the Prelude to reference the files with the .dhall extension; or to do validation on this task, which I can include in a follow-up PR. The purpose of this PR is to at least include this small feature

[sjakobi]

I'm aware they give 404 because we don't generate docs for files without .dhall extension. A solution would be to update the imports on the Prelude to reference the files with the .dhall extension;

OK. I think it would be good if you could work on this, so we can more easily tell what works and what doesn't.

or to do validation on this task, which I can include in a follow-up PR.

That also seems like a good idea to me.

I also noticed that the Prelude docs linked above don't include rendered header docs. Will that be fixed automatically once dhall-lang/dhall-lang#1045 is merged?

[german1608]

OK. I think it would be good if you could work on this, so we can more easily tell what works and what doesn't.

Sure, I'll prepare the PR as soon as we merge this

That also seems like a good idea to me.

I also noticed that the Prelude docs linked above don't include rendered header docs. Will that be fixed automatically once dhall-lang/dhall-lang#1045 is merged?

We will need to update the following lines

dhall-haskell/nix/dhall-docs-gen.nix

Lines 6 to 9 in 97ff185

	src = fetchurl {
	url = "https://github.com/german1608/dhall-lang/archive/feat/add-dhall-extensions-to-prelude.zip";
	sha256 = "ade9544719a26b7f3bf008572a794cb3878f284429d425a6c6a2e31c61189619";
	};

The generator doesn't use the latest commit from master, I couldn't find out a way to specify a src without sha256. I can update the reference after dhall-lang/dhall-lang#1045 is merged

[sjakobi]

A few initial comments.

BTW, I'm not very sad that the syntax highlighting is gone – it's not a very important feature to me personally. I like that the source code is now rendered with the formatting that it was written with, IIUC. 👍

[sjakobi]

Thanks for addressing my first comments! I understand this better now! :)

[sjakobi]

This still feels a bit convoluted, but I think I get the general idea.

Maybe it would be worth splitting out a pure function that takes care of the alignment of imports. Roughly like

alignAnnotations
    :: Text
    -> [(Int, ann)] -- ^ (Line number, annotation), line numbers must be ascending
    -> [(Text, [ann])] -- ^ Lines of the original Text, with annotations for each line

Then you can just fold over the resulting annotated lines and handle them in a uniform fashion.

[sjakobi]

Oh, in alignAnnotations, what I called the column numbers actually are the line numbers. I had mixed up the terms!

[german1608]

Sorry @sjakobi, but I don't get your idea 😕

[german1608]

what I do in a high-level is traversing the text, using the first argument of go as the cursor. The [Text] argument is used as the remainder of the text consume, the first line is not the whole line if the cursor column is different than 1.

We consume the prefix of the import position and render it as plain-text, render the import using a link if makes sense, and finally recur with the remainder of the text.

EDIT: Also note that a single import can span several lines, if it uses headers, for example.

[german1608]

(Probably this idea is what you suggested at first glance, sorry for that!)

We could take the source text and partitionate it using a custom data type:

data SourceCodeAnn = Normal Text | Link Text Import

-- if we concatenate the `SourceCodeAnn`'s `Text` we should get the input `Text`
partitionate :: Text -> [SourceCodeAnn]

render :: [SourceCodeAnn] -> Html ()

[sjakobi]

Yes, that's what I meant. SourceCodeAnn is a homomorphism of (Text, Maybe Import). I had suggested multiple imports / annotations because each line can contain multiple imports. When imports can also span multiple lines, things probably get a bit more complicated. No idea whether it's worthwhile.

[german1608]

I can try this in a follow-up PR. Remember that we also want to support jump-to-definition on other language elements, so probably this code will suffer changes.

[Gabriella439]

Sorry that I didn't get to this earlier because I was busy preparing for a talk, but I just wanted to say great job on doing this! 🙂