Scope info does not provide links for the openings

[pnlph]

When calling the go-to-definition command i am getting the links to the definitions but not to the openings, but it seems that the link should be there because of the wording:

Scope info

ℕ is in scope as
  * a data type Agda.Builtin.Nat.Nat brought into scope by
    - the opening of Data.Nat at
    - the opening of Data.Nat.Base at
    - the opening of Agda.Builtin.Nat at
    - its definition at 🔗 Agda-2.6.1/lib/prim/Agda/Builtin/Nat.agda:8,6-9
  * a module Agda.Builtin.Nat.Nat brought into scope by
    - the opening of Data.Nat at
    - the opening of Data.Nat.Base at
    - the opening of Agda.Builtin.Nat at
    - its definition at 🔗 Agda-2.6.1/lib/prim/Agda/Builtin/Nat.agda:8,6-9

I post it here because in agda/agda#4342 was explained that go-to-definition is an agda-modecommand.

[banacorn]

I'm picturing a dropdown list of links (like in fuzzy search shift-cmd-p) when there are multiple sources of definition. I've seen other languages doing the same thing. Would that be what you're expecting?

[pnlph]

I am actually very happy with the explicited list of openings. It gives a good overview on how the definition/module is linked to the structure of the library in use.

Even if the dropdown would save screen space, it would make more difficult to visualize the chain of imports.

Anyways, I share with you some useful generic design guidelines for dropdowns

[banacorn]

I'm thinking about making a module in the text a link, so that people can also access the intermediate openings

[pnlph]

Yes, makes sense. As a use case for its utility, I get the following when getting the scope info of Universes within the repository https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes

Scope info
Universe is in scope as
  * a defined name Agda.Primitive.Level brought into scope by
    - the opening of Universes at
    - the opening of Agda.Primitive at
    - its definition at /usr/local/Cellar/agda/2.6.1/share/x86_64-osx-ghc-8.8.3/Agda-2.6.1/lib/prim/Agda/Primitive.agda:17,3-8

There is a renaming of Level to Universe that is defined in the import statement of the file Universes.agda

A link to the Universes file would be useful in this case.

The open question is if it is better to have the text of the module linked or if the link should be explicited like in the definition (eg. to copy and paste easily to the Terminal app).