From 9d36d91b843f23ba4e02bbb5fa5836f9b14b7986 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Oct 2020 16:33:42 -0700
Subject: [PATCH] chore: add `Elab.command` trace class

---
 src/Lean/Elab/Command.lean                       |  4 +++-
 tests/lean/sanitizeMacroScopes.lean.expected.out | 14 +++-----------
 2 files changed, 6 insertions(+), 12 deletions(-)

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: <not-available>, 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: <not-available>, term
   m x
-  [Elab.step] 
-    [Elab.step] expected type: <not-available>, term
+  [Elab.step] expected type: <not-available>, term
     fun x✝ => x
-    [Elab.step] 
-      [Elab.step] expected type: Sort _, term
+    [Elab.step] expected type: Sort _, term
       _
-      [Elab.step] 
       [Elab.step] expected type: <not-available>, term
       x
-      [Elab.step] 
-[Elab.step] end