diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 21576bb7ce..b045914ea1 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -182,6 +182,8 @@ catch ex => match ex with let idName ← liftIO $ id.getName; logError msg!"internal exception {idName}" +initialize registerTraceClass `Elab.command + partial def elabCommand : Syntax → CommandElabM Unit | stx => withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with | Syntax.node k args => @@ -190,7 +192,7 @@ partial def elabCommand : Syntax → CommandElabM Unit -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones args.forM elabCommand else do - trace `Elab.step fun _ => stx; + trace `Elab.command fun _ => stx; let s ← get let stxNew? ← catchInternalId unsupportedSyntaxExceptionId (do let newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx)) diff --git a/tests/lean/sanitizeMacroScopes.lean.expected.out b/tests/lean/sanitizeMacroScopes.lean.expected.out index d4f2764cdd..0ccf9f7d84 100644 --- a/tests/lean/sanitizeMacroScopes.lean.expected.out +++ b/tests/lean/sanitizeMacroScopes.lean.expected.out @@ -1,21 +1,13 @@ -[Elab.step] #check fun x => m x fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m [Elab.step] expected type: , term fun x => m x -[Elab.step] - [Elab.step] expected type: Sort _, term +[Elab.step] expected type: Sort _, term _ - [Elab.step] [Elab.step] expected type: , term m x - [Elab.step] - [Elab.step] expected type: , term + [Elab.step] expected type: , term fun x✝ => x - [Elab.step] - [Elab.step] expected type: Sort _, term + [Elab.step] expected type: Sort _, term _ - [Elab.step] [Elab.step] expected type: , term x - [Elab.step] -[Elab.step] end