fix: emit info tree on command without elaborator

Fixes #792

src/Lean/Elab/Command.lean

@@ -274,7 +274,9 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
               elabCommand stxNew
         | _ =>
           match commandElabAttribute.getEntries s.env k with
-          | []      => throwError "elaboration function for '{k}' has not been implemented"
+          | []      =>
+            withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <|
+              throwError "elaboration function for '{k}' has not been implemented"
           | elabFns => elabCommandUsing s stx elabFns
     | _ => throwError "unexpected command"
 

tests/lean/infoTree.lean

@@ -37,3 +37,5 @@ def f5 (x : Nat) : B := {
 open Nat in
 #print xor
 instance : Inhabited Nat where
+
+macro

tests/lean/infoTree.lean.expected.out

@@ -318,5 +318,7 @@ bitwise bne
   command @ ⟨38, 0⟩-⟨38, 10⟩ @ Lean.Elab.Command.elabPrint
     xor : Nat → Nat → Nat @ ⟨38, 7⟩-⟨38, 10⟩
   command @ ⟨37, 0⟩†-⟨38, 10⟩† @ Lean.Elab.Command.elabEnd
-infoTree.lean:40:0: error: unexpected end of input; expected identifier
+infoTree.lean:41:0: error: expected identifier or term
 [Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ no_elab
+infoTree.lean:42:0: error: unexpected end of input
+[Elab.info] command @ ⟨41, 0⟩-⟨41, 5⟩ @ no_elab