No `goalsAccomplished` message is produced for theorems generated using `elab`

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

If I use elab to generate a theorem, Visual Studio Code does not display a checkmark in the left column when the theorem is proven.

The checkmark doesn't appear because Lean doesn't generate a goalsAccomplished message, which should happen in logGoalsAccomplishedSnapshotTask in Lean/Elab/MutalDef.lean.

Context

I originally pointed out this problem in a message on Lean Zulip.

Steps to Reproduce

import Lean
open Lean.Elab.Command

elab "bar" : command => do
  let c ← `(example: 0 = 0 := by trivial)
  elabCommand c

bar   -- no checkmark

Note that if a macro generates a theorem, a checkmark does appear as expected:

macro "foo" : command =>
  `(example: 0 = 0 := by trivial)

foo    -- checkmark appears in left column

Expected behavior:

A checkmark appears in the left column in VS Code, indicating that the theorem was proved.

Actual behavior:

There is no checkmark.

Versions

4.35.0 prerelease, built from git master at c155094f54eab345cca3da867dbd888a34fbf0d2

Start with the minimal examples in the issue and compare the macro-generated theorem with the theorem produced by elab. Read Lean/Elab/MutalDef.lean, especially logGoalsAccomplishedSnapshotTask, to trace why the goalsAccomplished message is missing. Done means the elab example produces a VS Code checkmark like the macro example.