Goals in traces are not properly indented

[JLimperg]

When displaying a goal as as part of a trace message, the goal is always fully dedented, even if it is within an indented trace node. This is mildly annoying since it breaks the hierarchical structure of the trace messages. Emacs does not have this issue.

MWE:

import Lean

open Lean Lean.Elab.Tactic

elab "test" : tactic => do
  withTraceNode `debug (λ _ => return "Section") do
    trace[debug] "The goal:{← getMainGoal}"

set_option trace.debug true in
example (h₁ : α) (h₂ : β) (h₃ : γ) : α := by
  test
    -- [debug] Section ▼
    --   [] The goal:
    -- h₁: α
    -- h₂: β
    -- h₃: γ
    -- ⊢ α