Showing two doc-string

Stream: general

[Damiano Testa]

Given the immediate success of my previous teaching inspired question, let me try something else.

This is about hover and, specifically, the declModifier hover and the protected hover in the code below:

import Lean

/-- This is just the multiplication of a group -/  -- <--- hover for information about `docComment`
class MyGroup where
  protected  -- <--- hover for information about `declModifiers`
    mul : G → G → G

[Damiano Testa]

Here are my observations/questions/feature requests:

• the hover information is great, I really love it and I wish it was available everywhere in the world!
• I would have liked that protected had some "protected-specific" hover -- I may PR something for that, since it is likely just a matter of adding a doc-string here.
• However, if I did that, where would I be able to see the very useful declModifiers doc-string?

[Damiano Testa]

This is where this question turns into a feature request: is there a way of getting a "primary" doc-string that would show what a docComment is when hovering over it, but also give the option of clicking/expanding a hover about declModifiers?

[Damiano Testa]

Ideally, every declModifier would have a doc-string, and then the declModifier doc-string would never show up in a hover!

[Marc Huisinga]

Damiano Testa said:

This is where this question turns into a feature request: is there a way of getting a "primary" doc-string that would show what a docComment is when hovering over it, but also give the option of clicking/expanding a hover about declModifiers?

Not right now, no.

In VS Code, enabling HTML support in the LSP client would enable us to put <details> tags in hovers which could then perhaps be used by the language server to hide optional "secondary" hover information (unclear what that would look like as of now). With enabled HTML support, we can already try the following:

/--
A short description of `foo`

<details>
<summary>This unfolds a bunch of details about `foo`</summary>

A

bunch

of

details

about

`foo`
</details>
-/
def foo := 1

#eval foo

Unfortunately, the UX of collapsed text in hovers in VS Code is pretty bad. On hover, we get the following hover panel:
image.png

Clicking the button changes the hover panel to the following:
image.png

Note that we can't see the unfolded text because VS Code did not resize the hover panel to fit the content after we expanded the <details> tag.
We first need to manually resize the hover panel by dragging the top right corner of the hover panel to see the hidden details:
image.png

So, this is technically possible, but the VS Code UX for it is pretty bad. It's also not clear to me whether other editors (e.g. NeoVim) will be able to work with HTML output by the language server.

[Damiano Testa]

Ok, thanks for investigating this so quickly! I agree that the screenshots that you showed are not a clear improvement and the hovers are currently great, so I would not want to switch to something not as good!

[David Thrane Christiansen]

I think that, very soon, the specific docstring for protected can contain a link to this page, which will be able to provide further information.

[David Thrane Christiansen]

Generally, I think hovers are great for a quick reminder about what something does, but a more in-depth description quickly outgrows them. Would something like that work for you too?

[Damiano Testa]

Ah, the verso-way! That would be also a great addition and would indeed be a perfect answer to my hover question!

[David Thrane Christiansen]

Great to hear! I'll get back to work :-)

[Damiano Testa]

I agree that hovers are more like bookmarks, so if they come with links to actual documentation that would be perfect.