pretty-printing the `conv` focusing dot

Stream: lean4

[Damiano Testa]

The focusing dot for conv seems to be defined as

/-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
macro dot:patternIgnore("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) })

Lean.Parser.Tactic.Conv.«conv·._»
I wonder if there should be spaces after each one of the two dots · and . for better pretty-printing.

Here is an example:

import Lean

open Lean.Parser.Tactic.Conv in
macro dot:patternIgnore("× " <|> "- ") s:convSeq : conv => `(conv| {%$dot ($s) })

open Lean Elab Command in
/-- shows the pretty-printed version of the following command -/
elab "#pretty " cmd:command : command => do
  elabCommand cmd
  logInfo (← liftCoreM do PrettyPrinter.ppCategory `command cmd)

/-
example : 0 = 0 := by
  conv =>
    congr
    × rfl   -- I would expect this
    ·rfl    -- rather than this
-/
#pretty
example : 0 = 0 := by
  conv =>
    congr
    × rfl
    · rfl