From 4e10e4e02ea2f166382491c38cbbb30e18d3f310 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 18 Feb 2025 07:58:47 +0000 Subject: [PATCH] feat: make linter names clickable in trace messages (#7119) This PR makes linter names clickable in the `trace.profiler` output. --- src/Lean/Elab/Command.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 525ce03205..00155f9392 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -274,7 +274,7 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do let linters ← lintersRef.get unless linters.isEmpty do for linter in linters do - withTraceNode `Elab.lint (fun _ => return m!"running linter: {linter.name}") + withTraceNode `Elab.lint (fun _ => return m!"running linter: {.ofConstName linter.name}") (tag := linter.name.toString) do let savedState ← get try @@ -282,7 +282,7 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do catch ex => match ex with | Exception.error ref msg => - logException (.error ref m!"linter {linter.name} failed: {msg}") + logException (.error ref m!"linter {.ofConstName linter.name} failed: {msg}") | Exception.internal _ _ => logException ex finally