From 13fb60f8a35e994d82881ad9f8a77e8530bb1260 Mon Sep 17 00:00:00 2001 From: Henrik Date: Fri, 8 Sep 2023 23:06:56 +0200 Subject: [PATCH] feat: deprecated attr --- DocGen4/Process/Attributes.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index 14d3336..ff6e7f3 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -124,7 +124,15 @@ def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (att return res def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes -def getParametricValues (decl : Name) : MetaM (Array String) := getValues decl parametricAttributes +def getParametricValues (decl : Name) : MetaM (Array String) := do + let mut uniform ← getValues decl parametricAttributes + -- This attribute contains an `Option Name` but we would like to pretty print it better + if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then + let str := match depTag with + | some alt => s!"deprecated {alt.toString}" + | none => "deprecated" + uniform := uniform.push str + return uniform def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do let insts ← getDefaultInstances className