From 0a2a8e8aa41d4efdb6d71fec0d68aeaa7693bcb6 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 1 Dec 2024 11:12:42 -0800 Subject: [PATCH] feat: make "foo has been deprecated" warning be hoverable (#6273) This PR modifies the "foo has been deprecated: use betterFoo instead" warning so that foo and betterFoo are hoverable. --- src/Lean/Linter/Deprecated.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean index ff248cc620..e9ac7a1ee2 100644 --- a/src/Lean/Linter/Deprecated.lean +++ b/src/Lean/Linter/Deprecated.lean @@ -51,8 +51,8 @@ def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [M if getLinterValue linter.deprecated (← getOptions) then let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure () logWarning <| .tagged ``deprecatedAttr <| - s!"`{declName}` has been deprecated" ++ match attr.text? with + m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with | some text => s!": {text}" | none => match attr.newName? with - | some newName => s!": use `{newName}` instead" + | some newName => m!": use `{.ofConstName newName true}` instead" | none => ""