Waiting on `elabCommand` in meta code?

Stream: lean4

[Thomas Murrills]

What's the right way to wait for a usage of elabCommand cmd in meta code, so that all messages and/or infotrees produced while elaborating cmd are available in the command state for inspection by subsequent meta code?

runLintersAsync does

  -- linters should have access to the complete info tree and message log
  let mut snaps := (← get).snapshotTasks
  if let some elabSnap := (← read).snap? then
    snaps := snaps.push { stx? := none, cancelTk? := none, task := elabSnap.new.result!.map (sync := true) toSnapshotTree }
  let tree := SnapshotTree.mk { diagnostics := .empty } snaps
  let treeTask ← tree.waitAll

But I'm not sure if this is specialized to post-elaboration at the top level somehow, and shouldn't be used in the middle of what might be a normal command elaborator itself. I'm a little wary of getting and resolving the elabSnap from the whole command context.

There are also mentions of withAlwaysResolvedPromises in source code comments, though I cannot find a declaration with that name (and am not sure if it's really related).