diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 3cc6e8be99..eb05141d39 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -297,11 +297,14 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do | elabFns => elabCommandUsing s stx elabFns | _ => throwError "unexpected command" +builtin_initialize registerTraceClass `Elab.input + /-- `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after macro expansion etc. -/ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do + trace[Elab.input] stx let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} }) let initInfoTrees ← getResetInfoTrees -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error