Try This suggestion styling

Stream: lean4

[Thomas Murrills]

Is Try This suggestion styling intended to be gone for good, or was it just not re-implemented in lean4#9966?

The reasoning given for deprecating it in the PR is that the hint infrastructure uses diff colors, but try this suggestions typically (still) do not use a diff. Styling was used in hint to communicate successful tactics.

@Marc Huisinga, is there any chance suggestion styling will eventually come back? (Currently, we're wondering whether to leave an adaptation note for hint in #nightly-testing > Mathlib status updates .)

[Marc Huisinga]

I'd prefer hints to be styled consistently (color-wise), but I'm happy to re-consider if use-cases other than hint end up popping up in practice.

but try this suggestions typically (still) do not use a diff

They now use blue to signal an insertion.

[Thomas Murrills]

I can appreciate that! I’ll mention two cases (ish) which come to mind:

This recent project is hint-like, and uses styling for a similar reason—but uses their own tweaked try this widget, and so is only really an example of how more hint-like tactics might come to exist.

One use case I had been meaning to get around to implementing was styling exact? suggestions which use deprecated constants with the deprecation styling.

They now use blue

For me, they’ve always been blue…I think they’ve always been styled as links to signal clickability, no?