how to configure jump to definition

Stream: mathlib4

[Floris van Doorn]

If I write an attribute/command/tactic that adds a new declaration to the environment, I noticed that there are two ways that I can configure "jump-to-definition" to work

• add declaration ranges with addDeclarationRanges
• add TermInfo with e.g. addTermInfo with isBinder := true

Is there a preferred way to do this? How do the two options relate (does one of them call the other, or are there multiple systems to decide to which definition to jump)? Is the second option abusing the isBinder option (since the doc string for addTermInfo suggests it's only for local constants)?

[Mario Carneiro]

You should do both

[Mario Carneiro]

Declaration ranges are for global jump to definition, e.g from different files, while the termInfo gives you a hover on the span of the declaration id showing the type of the declared constant

[Mario Carneiro]

I interpret the isBinder := true option more broadly, as "this is a declaration" vs "this is a use" for LSP purposes

[Floris van Doorn]

Ok, so the isBinder := true will only enable jump-to-definition for the current file? That makes sense if it's intended for local constants.
So we should use both, and set isBinder := true if it is the place where the new declaration is declared/introduced?

[Floris van Doorn]

What is the difference between range and selectionRange in DeclarationRanges?
Also, in the Alias tactic we have

  for a in aliases do withRef a do
    <stuff that doesn't change variable a>
    addDeclarationRanges declName {
      range := ← getDeclarationRange (← getRef)
      selectionRange := ← getDeclarationRange a
    }

am I correct that those two fields receive the same value?

[Floris van Doorn]

Suppose someone writes @[simps] that adds two declarations to the environment. Is there a way to show the TermInfo for both declarations on that attribute? (I can do it if someone passes two arguments as in @[simps fst snd] by showing an TermInfo on each of the arguments.)

[Wojciech Nawrocki]

@Floris van Doorn iirc range is the range of the whole definition whereas selectionRange is what gets selected when you jump to it. For example in

def frob := 37

range is the whole thing whereas selectionRange is frob.

[Floris van Doorn]

Ok, that is clarifying. Just curious: what is range used for? (What goes wrong if I set it wrong?)

[Wojciech Nawrocki]

The LSP spec says "This information is typically used to highlight the range in the editor." and I could swear it used to actually do this (the whole range would flash briefly) but it doesn't seem to do so currently. I might be having false memories, too.

[Mario Carneiro]

if I ctrl-hover over a declaration, the text in the span of range is shown in the hover