Try this regression in 4.24.0

Stream: lean4

[Eric Wieser]

In 4.23.0, I could use

def foo : Nat := show_term 1 + 2

and I would get two things in the infoview:
image.png

• A "Try this" suggestion which I could click to insert the term into the editor
• A regular message that contained an inspectable version of the 1 + 2 term, which allowed me to investigate which instance is being used in the middle of a larger term

In the latest Lean, this second item is gone, and it seems impossible to inspect the term of the "try this" suggestion because clicking it just accepts it.

[Marc Huisinga]

For context: this change was requested by people teaching with Lean because the duplicated information sometimes confuses students (lean4#9966), but I didn't notice that we are losing interactivity by doing this.

My proposal to fix this would be to move the link to apply the suggestion to the Try this:, change the (clickable) message to Try this (click to apply): and make the term after that interactive again. For Try these:, we'd have several terms with a clickable (click to apply) before them.

[Floris van Doorn]

I definitely like the removed duplication, and making the message in the Suggestions tab clickable seems perfect.

[Damiano Testa]

I also really like the deduplication and making the Try this clickable and the term hoverable seems great!

[Eric Wieser]

Perhaps instead of (click to apply), which is a bit verbose, an icon of some kind could work too, with that as hover text?

[Marc Huisinga]

Eric Wieser said:

Perhaps instead of (click to apply), which is a bit verbose, an icon of some kind could work too, with that as hover text?

I'd definitely prefer an icon as well, but I can't think of an obvious one that makes it absolutely clear to everyone that this is the icon that should be clicked. The best one I can come up with is a checkmark, and I don't think that will be clear enough.

[Damiano Testa]

What if instead of Try this it were Click this?

[Julian Berman]

Perhaps a broader thing to think through but I've thought it'd be nice if there were a "Show UX Hints" server setting (default on) which explains how to interact with various things which are "non-obvious", shift-click being the most notorious .But then if you turn it off then stuff should get "less noisy", e.g. not show even "Try this", just have it be link colored.

[Julian Berman]

Obviously that'd let the default be noisier since it'd be targeted to newer users.

[Marc Huisinga]

Damiano Testa said:

What if instead of Try this it were Click this?

The "Try this" case isn't really the tricky one here since I think using link coloring for it would probably already suffice. The various cases in "Try these" are the tricky part.

[Marc Huisinga]

Julian Berman said:

Perhaps a broader thing to think through but I've thought it'd be nice if there were a "Show UX Hints" server setting (default on) which explains how to interact with various things which are "non-obvious", shift-click being the most notorious .But then if you turn it off then stuff should get "less noisy", e.g. not show even "Try this", just have it be link colored.

FWIW, in the InfoView, we now provide context menu entries for most InfoView actions and options to make things more discoverable.

[Marc Huisinga]

lean4#10524

I ended up using an [apply] prefix for the link. I tried the checkmark icon idea above, but it also suffers from the fact that both the codicon checkmark icon and the checkmark emoji usually don't play nice with monospace fonts, so when a long suggestion is broken up by the pretty-printer, it won't be aligned with the line above. I hope that [apply] will suffice as a compromise between brevity and clarity.