RFC: Full name when clicking in infoview

Proposal

I propose that we display the full name of the constant when clicking in the infoview.

For example, consider the following code:

namespace Foo

axiom test : Nat

theorem bar : test = 0 := by
  sorry

end Foo

If you put your cursor before the sorry, and click on the test in the infoview, there is no way to see that it actually refers to Foo.test, which might cause it to be difficult to look up the correct lemmas. I propose that the output generated when clicking on test should be Foo.test.

Community Feedback

Zulip.

Someone asked if the full name should appear when clicked once or twice, and I said that I do not mind it either way. They also pointed out that this should be as easy as setting set_option pp.fullNames true when clicking on the infoview.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by tracing how the infoview handles clicks on identifiers and review the existing pp.fullNames option mentioned in the proposal. Done means that clicking test in the shown example presents the fully qualified name Foo.test, with the interaction behavior chosen consistently.