diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index dbf41b35a1..27c2fbedcf 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -11,11 +11,8 @@ import Init.Data.Array.Subarray import Init.Data.ToString namespace Lean -syntax "Macro.trace[" ident "]" interpolatedStr(term) : term - -macro_rules - | `(Macro.trace[$id] $s) => `(Macro.trace $(quote id.getId) (s! $s)) - +macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term => + `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s)) -- Auxiliary parsers and functions for declaring notation with binders diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 67ae1512e9..5614cb4f97 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -143,7 +143,7 @@ def registerTraceClass (traceClassName : Name) : IO Unit := macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do let msg ← if s.getKind == interpolatedStrKind then `(m! $s) else `(($s : MessageData)) `(doElem| do - let cls := $(quote id.getId) + let cls := $(quote id.getId.eraseMacroScopes) if (← Lean.isTracingEnabledFor cls) then Lean.addTrace cls $msg) diff --git a/tests/lean/traceClassScopes.lean b/tests/lean/traceClassScopes.lean new file mode 100644 index 0000000000..4ff8e70f55 --- /dev/null +++ b/tests/lean/traceClassScopes.lean @@ -0,0 +1,19 @@ +import Lean + +macro "t" t:interpolatedStr(term) : doElem => + `(Macro.trace[Meta.debug] $t) + +macro "tstcmd" : command => do + t "hello" + `(example : Nat := 1) + +set_option trace.Meta.debug true in +tstcmd + +open Lean Meta + +macro "r" r:interpolatedStr(term) : doElem => + `(trace[Meta.debug] $r) + +set_option trace.Meta.debug true in +#eval show MetaM _ from do r "world" diff --git a/tests/lean/traceClassScopes.lean.expected.out b/tests/lean/traceClassScopes.lean.expected.out new file mode 100644 index 0000000000..512b8343aa --- /dev/null +++ b/tests/lean/traceClassScopes.lean.expected.out @@ -0,0 +1,2 @@ +[Meta.debug] hello +[Meta.debug] world