feat: denote deprecations in completion items (#5707)

This PR ensures that deprecated declarations are displayed with a
strikethrough markup in the completion popup of VS Code and that the
docstring of a completion item denotes the meta-data of the deprecation.

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -41,6 +41,18 @@ structure InsertReplaceEdit where
   replace : Range
   deriving FromJson, ToJson
 
+inductive CompletionItemTag where
+  | deprecated
+  deriving Inhabited, DecidableEq, Repr
+
+instance : ToJson CompletionItemTag where
+  toJson t := toJson (t.toCtorIdx + 1)
+
+instance : FromJson CompletionItemTag where
+  fromJson? v := do
+    let i : Nat ← fromJson? v
+    return CompletionItemTag.ofNat (i-1)
+
 structure CompletionItem where
   label          : String
   detail?        : Option String := none
@@ -49,8 +61,8 @@ structure CompletionItem where
   textEdit?      : Option InsertReplaceEdit := none
   sortText?      : Option String := none
   data?          : Option Json := none
+  tags?          : Option (Array CompletionItemTag) := none
   /-
-  tags? : CompletionItemTag[]
   deprecated? : boolean
   preselect? : boolean
   filterText? : string
@@ -59,7 +71,8 @@ structure CompletionItem where
   insertTextMode? : InsertTextMode
   additionalTextEdits? : TextEdit[]
   commitCharacters? : string[]
-  command? : Command -/
+  command? : Command
+  -/
   deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where

src/Lean/Server/Completion.lean

@@ -167,14 +167,33 @@ private def addUnresolvedCompletionItem
     (kind          : CompletionItemKind)
     (score         : Float)
     : M Unit := do
-  let doc? ← do
-    match id with
-    | .const declName =>
-      let docString? ← findDocString? (← getEnv) declName
-      pure <| docString?.map fun docString =>
-        { value := docString, kind := MarkupKind.markdown : MarkupContent }
-    | .fvar _ => pure none
-  let item := { label := label.toString, kind? := kind, documentation? := doc? }
+  let env ← getEnv
+  let (docStringPrefix?, tags?) := Id.run do
+    let .const declName := id
+      | (none, none)
+    let some param := Linter.deprecatedAttr.getParam? env declName
+      | (none, none)
+    let docstringPrefix :=
+      if let some text := param.text? then
+        text
+      else if let some newName := param.newName? then
+        s!"`{declName}` has been deprecated, use `{newName}` instead."
+      else
+        s!"`{declName}` has been deprecated."
+    (some docstringPrefix, some #[CompletionItemTag.deprecated])
+  let docString? ← do
+    let .const declName := id
+      | pure none
+    findDocString? env declName
+  let doc? := do
+    let docValue ←
+      match docStringPrefix?, docString? with
+      | none,                 none           => none
+      | some docStringPrefix, none           => docStringPrefix
+      | none,                 docString      => docString
+      | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}"
+    pure { value := docValue , kind := MarkupKind.markdown : MarkupContent }
+  let item := { label := label.toString, kind? := kind, documentation? := doc?, tags?}
   addItem item score id
 
 private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do

tests/lean/interactive/completionDeprecation.lean

@@ -0,0 +1,27 @@
+structure SomeStructure where
+  n : Nat
+
+def SomeStructure.foo1 (s : SomeStructure) : Nat := s.n
+
+/-- A docstring. -/
+def SomeStructure.foo2 (s : SomeStructure) : Nat := s.n
+
+@[deprecated] def SomeStructure.foo3 (s : SomeStructure) : Nat := s.n
+
+/-- A docstring. -/
+@[deprecated] def SomeStructure.foo4 (s : SomeStructure) : Nat := s.n
+
+@[deprecated SomeStructure.foo1] def SomeStructure.foo5 (s : SomeStructure) : Nat := s.n
+
+/-- A docstring. -/
+@[deprecated SomeStructure.foo1] def SomeStructure.foo6 (s : SomeStructure) : Nat := s.n
+
+@[deprecated "`SomeStructure.foo7` has been deprecated; please use `SomeStructure.foo1` instead."]
+def SomeStructure.foo7 (s : SomeStructure) : Nat := s.n
+
+/-- A docstring. -/
+@[deprecated "`SomeStructure.foo8` has been deprecated; please use `SomeStructure.foo1` instead."]
+def SomeStructure.foo8 (s : SomeStructure) : Nat := s.n
+
+example := SomeStructure.foo  -- Completion items with a deprecation tag and a deprecation message
+                          --^ textDocument/completion

tests/lean/interactive/completionDeprecation.lean.expected.out

@@ -0,0 +1,96 @@
+{"textDocument": {"uri": "file:///completionDeprecation.lean"},
+ "position": {"line": 25, "character": 28}}
+{"items":
+ [{"sortText": "0",
+   "label": "foo1",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo1"}}}},
+  {"sortText": "1",
+   "label": "foo2",
+   "kind": 3,
+   "documentation": {"value": "A docstring. ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo2"}}}},
+  {"tags": [1],
+   "sortText": "2",
+   "label": "foo3",
+   "kind": 3,
+   "documentation":
+   {"value": "`SomeStructure.foo3` has been deprecated.", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo3"}}}},
+  {"tags": [1],
+   "sortText": "3",
+   "label": "foo4",
+   "kind": 3,
+   "documentation":
+   {"value": "`SomeStructure.foo4` has been deprecated.\n\nA docstring. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo4"}}}},
+  {"tags": [1],
+   "sortText": "4",
+   "label": "foo5",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "`SomeStructure.foo5` has been deprecated, use `SomeStructure.foo1` instead.",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo5"}}}},
+  {"tags": [1],
+   "sortText": "5",
+   "label": "foo6",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "`SomeStructure.foo6` has been deprecated, use `SomeStructure.foo1` instead.\n\nA docstring. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo6"}}}},
+  {"tags": [1],
+   "sortText": "6",
+   "label": "foo7",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "`SomeStructure.foo7` has been deprecated; please use `SomeStructure.foo1` instead.",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo7"}}}},
+  {"tags": [1],
+   "sortText": "7",
+   "label": "foo8",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "`SomeStructure.foo8` has been deprecated; please use `SomeStructure.foo1` instead.\n\nA docstring. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionDeprecation.lean"},
+     "position": {"line": 25, "character": 28}},
+    "id": {"const": {"declName": "SomeStructure.foo8"}}}}],
+ "isIncomplete": true}