Trythis code action title

Stream: std4

[Patrick Massot]

When creating a Try this widget, you can provide a header to replace the default "Try this". However this header is hard-wired in the action provider. I guess this is an oversight. Is there any hidden deep reason for this? Or should I try to fix it and PR it to std$?

[Scott Morrison]

PR please!

[Kyle Miller]

Speaking of TryThis, I know that the says tactic uses the "try this" header. Maybe if the Suggestion's message data were wrapped in docs#Lean.MessageData.tagged then it could more reliably extract the suggestion. Maybe this instance could insert that tagging: https://github.com/leanprover/std4/blob/c4aef3c27c6df946c46ac52564c84c86e2ccd2cc/Std/Tactic/TryThis.lean#L160

I don't really know what tagging is used for, but I noticed that docs#Lean.Elab.Term.reportUnsolvedGoals tags the message.

[Thomas Murrills]

The reason I (deliberately) left it as Try this: in (just) the code action was because code actions are best as one-liners and we’re visually short on space there, and (imo) there’s value in communicating the nature of the action itself in a brief, direct, and standard way. Having only “Try this:” before the replacement syntax was (I figured) a sufficiently basic, familiar, and to-the-point way to communicate “replace the squiggled text with the given text” in as little space as possible. If someone includes a long header or other non-replacement text in their suggestion, it shouldn’t obstruct the user’s view of what the code action will do in the lightbulb menu. (Also, I didn’t want to make that PR any bigger than it was by including even more knobs to fiddle with.)

Note that we also can’t simply use the header argument itself: you don’t want each individual code action to say “Try these: <replacement>” in the addSuggestions case.

But! If we want flexibility here (and we probably do, after all) we could add a field to Suggestion like codeActionString : Option (Suggestion → String) := none. Then you can include whatever aspects of the suggestion you want in whatever way you want to, or you can just use the default.

(Actually I need to check this makes sense; maybe we don’t want to format the syntax twice, or maybe we don’t have access to the suggestion when needed, etc. Maybe we just want to offer codeAction : Option (String → String) or simply codeActionPrefix : Option String or something, or even just a uniform prefix that gets passed as a prop instead of as a suggestion field (even though each suggestion gets its own code action).)

(There’s also the question of whether we agree with this default behavior I’ve adopted in the first place, though.)

[Patrick Massot]

It all make sense for expert usage, but the context of my question was teaching in another language than English.

[Thomas Murrills]

std4#466

[Thomas Murrills]

Makes sense! My perspective was admittedly limited to the considerations above when thinking about the behavior initially. :)

In the PR I add a field toCodeActionTitle? : Option (String → String) to Suggestion which can be applied to the pretty-printed suggestion text (in general, this could also be used to, for example, dependently include the number of remaining goals resulting from a tactic execution: "Try this: (⊢ 3) <tactic replacement>" or "Try this: :tada: <tactic replacement>") and a convenient argument codeActionPrefix? : Option String := none for addSuggestions which is used as a prefix to the suggestion text by default (if toCodeActionTitle? is not provided).