fix: support more parsers in `#help`

[digama0]

As reported on Zulip, the #help command is out of date with respect to the parsers that can be obscuring the search for the "first token", used to power the search-by-token-prefix form of the command #help tactic "measur". The list below has been tested against everything in lean, and the only things that fail to find a first token now are those that actually don't have a token like the ident parser.

---

[grunweg]

AIUI, this is blocked on the author fixing the build failures - let me label it as such.

[robertylewis]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style