feat: print diagnostics from command elabs

Mathport/Syntax/Translate/Command.lean

@@ -567,8 +567,7 @@ def trNotationCmd (loc : LocalReserve) (attrs : Attributes) (nota : Notation)
   let n4 ← Elab.Command.withWeakNamespace (ns ++ (← getEnv).mainModule) $ do
     let n4 ← mkUnusedName nota.name4
     let nn ← `(Parser.Command.namedName| (name := $(mkIdent n4)))
-    try elabCommand (cmd (some nn) e).1
-    catch e => dbg_trace "warning: failed to add syntax {repr n4}: {← e.toMessageData.toString}"
+    Elab.withLogging do elabCommand (cmd (some nn) e).1
     pure $ (← getCurrNamespace) ++ n4
   printOutput s!"-- mathport name: {n}\n"
   if ns == default then push (cmd none e).1
@@ -596,7 +595,7 @@ def trAttributeCmd (loc : Bool) (attrs : Attributes) (ns : Array (Spanned Name))
   unless attrs.isEmpty do
     push $ f $ ← `(attribute [$attrs,*] $ns*)
 
-def trCommand' : Command → M Unit
+def trCommand'' : Command → M Unit
   | Command.initQuotient => pushM `(init_quot)
   | Command.mdoc doc =>
     push $ mkNode ``Parser.Command.moduleDoc #[mkAtom "/-!", mkAtom (doc ++ "-/")]
@@ -679,3 +678,9 @@ def trCommand' : Command → M Unit
     match (← get).userCmds.find? n with
     | some f => try f mods args catch e => warn! "in {n} {repr args}: {← e.toMessageData.toString}"
     | none => warn! "unsupported user command {n}"
+
+def trCommand' (cmd : Command) : M Unit := do
+  trCommand'' cmd
+  let msgs ← modifyGetThe Elab.Command.State fun st => (st.messages, { st with messages := {} })
+  for msg in msgs.msgs do
+    logComment (← msg.toString)