chore: wrap diagnostic results in MessageData.traces

[mattrobball]

Currently, the messages in the diagnostic summaries are created by appending interpolated strings. We wrap these in .trace's, and the results are better formatted when expanding child nodes in the info view. Particularly, the latter diagnostic summaries remain on their own lines flush to the left instead of on the same line directly adjacent to the last child node.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-08-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-08-01 15:16:57)

[leodemoura]

@mattrobball The new output looks good to me. Ready to merge?

[mattrobball]

Yes, thanks.