max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make "foo has been deprecated" warning be hoverable (#6273)

Browse source 
This PR modifies the "foo has been deprecated: use betterFoo instead"
warning so that foo and betterFoo are hoverable.
This commit is contained in:
Kyle Miller 2024-12-01 11:12:42 -08:00 • committed by GitHub
parent 23236ef520
commit 0a2a8e8aa4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Linter/Deprecated.lean
View file

@ -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 => ""