Minor simp? annoyances

Stream: lean4

[Michael Stoll]

1. · simp?: the "Try this:" suggestion does not indent the lines after the first.
2. simp? +contextual gives simp+contextual only .... Is the missing space after simp intentional? (The syntax seems to parse, in any case.)
3. simp? does not work in conv mode.

Can these be addressed at some point? The last one is the most annoying, but I imagine the hardest to fix.

[Kyle Miller]

2. lean4#6161

[Kim Morrison]

@Michael Stoll, would you mind opening issues for 1. and 3.?

[Michael Stoll]

lean4#6163 for the first point.

[Michael Stoll]

lean4#6164 for the third.

[Michael Stoll]

Here is another point.

4. The "Try this" code replacement tends to put line breaks between ← and the following lemma name (which parses OK, but is hard to read).