Commit 2026-10-17 01:01 fbc1661a
View on Github →feat(ClickSuggestions): use the tactic as the button text (#44894)
This PR updates the front end of #click_suggestions.
- Instead of using
[apply]for each suggestion button, we use the name of the used tactic, so either[apply],[rw]or[grw](and[exact]instead of[apply]if the application closes the goal). - The title of each section of results now displays e.g.
Pattern ?n + ?minstead ofrw (?n + ?m), which makes it clearer that the shown expression is a pattern. - Instead of displaying
[done]for suggestions that solve the goal, we add a🎉️emoji in front of it. - The list of tactic suggestions that close the goal still uses the
[done]button text. It doesn't need to say the tactic in the button text because the tactic is already shown next to the button.