Feature request: display namespace when clicking in infoview

Stream: lean4

[Kenny Lau]

namespace Foo

axiom test : Nat

theorem bar : test = 0 := by
  sorry

end Foo

image.png

[Kenny Lau]

When hovering over test in Line 3, the namespace Foo is displayed, but when one clicks on test that appears in the infoview, there is no way to get it to show Foo; my request is to have the printer show Foo.test when one clicks on it in the infoview

[Robin Arnez]

That would just mean set_option pp.fullNames true when you click on there I suppose

[Robin Arnez]

Yeah I also got annoyed at that a few times

[Robin Arnez]

The question is (for an application): Should this show when you click once or only when you click on the constant

[Kenny Lau]

once

[Robin Arnez]

So between these two:
Click once
Click twice
you'd choose the first one?

[Kenny Lau]

yes, but I don't really mind either way; either is better than the status quo

[Kenny Lau]

https://github.com/leanprover/lean4/issues/9992

[Kenny Lau]

so, I wanna revive this thread, how easy is this to implement?