RFC: try-this widget: multiple replacemens, alternative text in InfoView

Proposal

Multiple edits

I would be able to address #4546 in maybe the most preferable way if the the “Try this” functionality would allow multiple simultaneous replacements. In that issue, termination_by? on a function that is part of a mutually recursive clique should really add an termination_by annotation to every function in the group at once.

Alternative text in widget

And while I am at it: in other applications the replacement text became very large (dozens of lines), and I would have preferred control over the link text to be able to say, for example ((and 10 more lines…)) or something else completely.

Replacement links in MessageData instead of Widgets

(This is more brainststormy, but maybe worth considering at some point.)

Maybe there is even a way to make embed a try-this link part of MessageData that I can embed such actions right in the the corresponding logInfo or throwError. This would avoid the user seeing a message (under “Messages”) and a separate redundant thing (or many, as with tactics like apply?) under the new header “Try this” in the info view. It would also avoid the need of functions like addSuggestions that produce a list, and users can format multiple suggestions in whatever they prefer.

Having such a .editAction : (edits : Array (Syntax × String)) (label : MessageData) → MessageData is also a bit more “semantics“ than a Widget with embedded TypeScript code, so hopefully makes it easier to be supported by other editors, or to write tools that perform such edits. (I expect at some point we need a batch tool that updates the #guard_msgs docstrings in our test suite.)

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 with Lean.Meta.Tactic.TryThis.addSuggestions, the only entry point named in the issue, and trace how suggestions reach the Try this widget. Before implementation, resolve which of the three proposals is in scope; done should include agreed behavior for multiple edits, custom labels, or MessageData actions, with corresponding tests.