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 + ?m instead of rw (?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.

Estimated changes