diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out
index 12af05069f..ae0a4769c3 100644
--- a/tests/lean/interactive/533.lean.expected.out
+++ b/tests/lean/interactive/533.lean.expected.out
@@ -1,117 +1,229 @@
 {"textDocument": {"uri": "file://533.lean"},
  "position": {"line": 2, "character": 10}}
 {"items":
- [{"label": "False", "kind": 22, "detail": "Prop"},
-  {"label": "Fin", "kind": 22, "detail": "Nat → Type"},
-  {"label": "Float", "kind": 22, "detail": "Type"},
-  {"label": "FloatArray", "kind": 22, "detail": "Type"},
-  {"label": "FloatSpec", "kind": 22, "detail": "Type 1"},
-  {"label": "Foo", "kind": 6, "detail": "Sort ?u"},
-  {"label": "ForIn",
+ [{"textEdit": null,
+   "label": "False",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Prop"},
+  {"textEdit": null,
+   "label": "Fin",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Nat → Type"},
+  {"textEdit": null,
+   "label": "Float",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Type"},
+  {"textEdit": null,
+   "label": "FloatArray",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Type"},
+  {"textEdit": null,
+   "label": "FloatSpec",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Type 1"},
+  {"textEdit": null,
+   "label": "Foo",
+   "kind": 6,
+   "documentation": null,
+   "detail": "Sort ?u"},
+  {"textEdit": null,
+   "label": "ForIn",
    "kind": 7,
+   "documentation": null,
    "detail":
    "(Type u₁ → Type u₂) → Type u → outParam (Type v) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
-  {"label": "ForIn'",
+  {"textEdit": null,
+   "label": "ForIn'",
    "kind": 7,
+   "documentation": null,
    "detail":
    "(Type u₁ → Type u₂) →\n  (ρ : Type u) → (α : outParam (Type v)) → outParam (Membership α ρ) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
-  {"label": "ForInStep", "kind": 22, "detail": "Type u → Type u"},
-  {"label": "ForM",
+  {"textEdit": null,
+   "label": "ForInStep",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Type u → Type u"},
+  {"textEdit": null,
+   "label": "ForM",
    "kind": 7,
+   "documentation": null,
    "detail":
    "(Type u → Type v) → Type w₁ → outParam (Type w₂) → Type (max (max (max (u + 1) v) w₁) w₂)"},
-  {"label": "Function", "kind": 9, "detail": "namespace"},
-  {"label": "Functor",
+  {"textEdit": null,
+   "label": "Function",
+   "kind": 9,
+   "documentation": null,
+   "detail": "namespace"},
+  {"textEdit": null,
+   "label": "Functor",
    "kind": 7,
+   "documentation": null,
    "detail": "(Type u → Type v) → Type (max (u + 1) v)"},
-  {"label": "fix",
+  {"textEdit": null,
+   "label": "fix",
    "kind": 3,
+   "documentation": null,
    "detail": "[inst : Inhabited β] → ((α → β) → α → β) → α → β"},
-  {"label": "fix1",
+  {"textEdit": null,
+   "label": "fix1",
    "kind": 3,
+   "documentation": null,
    "detail": "[inst : Inhabited β] → ((α → β) → α → β) → α → β"},
-  {"label": "fix2",
+  {"textEdit": null,
+   "label": "fix2",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Inhabited β] → ((α₁ → α₂ → β) → α₁ → α₂ → β) → α₁ → α₂ → β"},
-  {"label": "fix3",
+  {"textEdit": null,
+   "label": "fix3",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Inhabited β] → ((α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β"},
-  {"label": "fix4",
+  {"textEdit": null,
+   "label": "fix4",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Inhabited β] → ((α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β"},
-  {"label": "fix5",
+  {"textEdit": null,
+   "label": "fix5",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Inhabited β] → ((α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β"},
-  {"label": "fix6",
+  {"textEdit": null,
+   "label": "fix6",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Inhabited β] →\n  ((α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β"},
-  {"label": "fixCore",
+  {"textEdit": null,
+   "label": "fixCore",
    "kind": 3,
+   "documentation": null,
    "detail": "(α → β) → ((α → β) → α → β) → α → β"},
-  {"label": "fixCore1",
+  {"textEdit": null,
+   "label": "fixCore1",
    "kind": 3,
+   "documentation": null,
    "detail": "(α → β) → ((α → β) → α → β) → α → β"},
-  {"label": "fixCore2",
+  {"textEdit": null,
+   "label": "fixCore2",
    "kind": 3,
+   "documentation": null,
    "detail": "(α₁ → α₂ → β) → ((α₁ → α₂ → β) → α₁ → α₂ → β) → α₁ → α₂ → β"},
-  {"label": "fixCore3",
+  {"textEdit": null,
+   "label": "fixCore3",
    "kind": 3,
+   "documentation": null,
    "detail":
    "(α₁ → α₂ → α₃ → β) → ((α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β"},
-  {"label": "fixCore4",
+  {"textEdit": null,
+   "label": "fixCore4",
    "kind": 3,
+   "documentation": null,
    "detail":
    "(α₁ → α₂ → α₃ → α₄ → β) → ((α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β"},
-  {"label": "fixCore5",
+  {"textEdit": null,
+   "label": "fixCore5",
    "kind": 3,
+   "documentation": null,
    "detail":
    "(α₁ → α₂ → α₃ → α₄ → α₅ → β) → ((α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β"},
-  {"label": "fixCore6",
+  {"textEdit": null,
+   "label": "fixCore6",
    "kind": 3,
+   "documentation": null,
    "detail":
    "(α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) →\n  ((α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β"},
-  {"label": "failure",
+  {"textEdit": null,
+   "label": "failure",
    "kind": 5,
+   "documentation": null,
    "detail": "[self : Alternative f] → {α : Type u} → f α"},
-  {"label": "false", "kind": 4, "detail": "Bool"},
-  {"label": "false_and",
+  {"textEdit": null,
+   "label": "false",
+   "kind": 4,
+   "documentation": null,
+   "detail": "Bool"},
+  {"textEdit": null,
+   "label": "false_and",
    "kind": 3,
+   "documentation": null,
    "detail": "∀ (p : Prop), (False ∧ p) = False"},
-  {"label": "false_iff", "kind": 3, "detail": "∀ (p : Prop), (False ↔ p) = ¬p"},
-  {"label": "false_implies",
+  {"textEdit": null,
+   "label": "false_iff",
    "kind": 3,
+   "documentation": null,
+   "detail": "∀ (p : Prop), (False ↔ p) = ¬p"},
+  {"textEdit": null,
+   "label": "false_implies",
+   "kind": 3,
+   "documentation": null,
    "detail": "∀ (p : Prop), (False → p) = True"},
-  {"label": "false_of_ne", "kind": 3, "detail": "a ≠ a → False"},
-  {"label": "false_or", "kind": 3, "detail": "∀ (p : Prop), (False ∨ p) = p"},
-  {"label": "flip", "kind": 3, "detail": "(α → β → φ) → β → α → φ"},
-  {"label": "floatDecLe",
+  {"textEdit": null,
+   "label": "false_of_ne",
    "kind": 3,
+   "documentation": null,
+   "detail": "a ≠ a → False"},
+  {"textEdit": null,
+   "label": "false_or",
+   "kind": 3,
+   "documentation": null,
+   "detail": "∀ (p : Prop), (False ∨ p) = p"},
+  {"textEdit": null,
+   "label": "flip",
+   "kind": 3,
+   "documentation": null,
+   "detail": "(α → β → φ) → β → α → φ"},
+  {"textEdit": null,
+   "label": "floatDecLe",
+   "kind": 3,
+   "documentation": null,
    "detail": "(a b : Float) → Decidable (a ≤ b)"},
-  {"label": "floatDecLt",
+  {"textEdit": null,
+   "label": "floatDecLt",
    "kind": 3,
+   "documentation": null,
    "detail": "(a b : Float) → Decidable (a < b)"},
-  {"label": "floatSpec", "kind": 21, "detail": "FloatSpec"},
-  {"label": "forIn",
+  {"textEdit": null,
+   "label": "floatSpec",
+   "kind": 21,
+   "documentation": null,
+   "detail": "FloatSpec"},
+  {"textEdit": null,
+   "label": "forIn",
    "kind": 5,
+   "documentation": null,
    "detail":
    "[self : ForIn m ρ α] → {β : Type u₁} → [inst : Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β"},
-  {"label": "forIn'",
+  {"textEdit": null,
+   "label": "forIn'",
    "kind": 5,
+   "documentation": null,
    "detail":
    "[self : ForIn' m ρ α d] → {β : Type u₁} → [inst : Monad m] → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β"},
-  {"label": "forM",
+  {"textEdit": null,
+   "label": "forM",
    "kind": 5,
+   "documentation": null,
    "detail":
    "[self : ForM m γ α] → [inst : Monad m] → γ → (α → m PUnit) → m PUnit"},
-  {"label": "forall_congr",
+  {"textEdit": null,
+   "label": "forall_congr",
    "kind": 3,
+   "documentation": null,
    "detail": "(∀ (a : α), p a = q a) → (∀ (a : α), p a) = ∀ (a : α), q a"},
-  {"label": "funext",
+  {"textEdit": null,
+   "label": "funext",
    "kind": 3,
+   "documentation": null,
    "detail": "(∀ (x : α), f₁ x = f₂ x) → f₁ = f₂"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out
index f084a6edeb..a5be6756fa 100644
--- a/tests/lean/interactive/863.lean.expected.out
+++ b/tests/lean/interactive/863.lean.expected.out
@@ -1,58 +1,88 @@
 {"textDocument": {"uri": "file://863.lean"},
  "position": {"line": 3, "character": 12}}
 {"items":
- [{"label": "getRecAppSyntax?",
+ [{"textEdit": null,
+   "label": "getRecAppSyntax?",
    "kind": 3,
    "documentation":
    {"value":
     "Retrieve (if available) the syntax object attached to a recursive application.\n",
     "kind": "markdown"},
    "detail": "Expr → Option Syntax"},
-  {"label": "getReducibilityStatus",
+  {"textEdit": null,
+   "label": "getReducibilityStatus",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
-  {"label": "getReducibilityStatusImp",
+  {"textEdit": null,
+   "label": "getReducibilityStatusImp",
    "kind": 3,
+   "documentation": null,
    "detail": "Environment → Name → ReducibilityStatus"},
-  {"label": "getRef", "kind": 5, "detail": "[self : MonadRef m] → m Syntax"},
-  {"label": "getRegularInitFnNameFor?",
+  {"textEdit": null,
+   "label": "getRef",
+   "kind": 5,
+   "documentation": null,
+   "detail": "[self : MonadRef m] → m Syntax"},
+  {"textEdit": null,
+   "label": "getRegularInitFnNameFor?",
    "kind": 3,
+   "documentation": null,
    "detail": "Environment → Name → Option Name"},
-  {"label": "getRevAliases",
+  {"textEdit": null,
+   "label": "getRevAliases",
    "kind": 3,
+   "documentation": null,
    "detail": "Environment → Name → List Name"},
-  {"label": "getConstInfoRec",
+  {"textEdit": null,
+   "label": "getConstInfoRec",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m RecursorVal"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://863.lean"},
  "position": {"line": 7, "character": 12}}
 {"items":
- [{"label": "getRecAppSyntax?",
+ [{"textEdit": null,
+   "label": "getRecAppSyntax?",
    "kind": 3,
    "documentation":
    {"value":
     "Retrieve (if available) the syntax object attached to a recursive application.\n",
     "kind": "markdown"},
    "detail": "Expr → Option Syntax"},
-  {"label": "getReducibilityStatus",
+  {"textEdit": null,
+   "label": "getReducibilityStatus",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
-  {"label": "getReducibilityStatusImp",
+  {"textEdit": null,
+   "label": "getReducibilityStatusImp",
    "kind": 3,
+   "documentation": null,
    "detail": "Environment → Name → ReducibilityStatus"},
-  {"label": "getRef", "kind": 5, "detail": "[self : MonadRef m] → m Syntax"},
-  {"label": "getRegularInitFnNameFor?",
+  {"textEdit": null,
+   "label": "getRef",
+   "kind": 5,
+   "documentation": null,
+   "detail": "[self : MonadRef m] → m Syntax"},
+  {"textEdit": null,
+   "label": "getRegularInitFnNameFor?",
    "kind": 3,
+   "documentation": null,
    "detail": "Environment → Name → Option Name"},
-  {"label": "getRevAliases",
+  {"textEdit": null,
+   "label": "getRevAliases",
    "kind": 3,
+   "documentation": null,
    "detail": "Environment → Name → List Name"},
-  {"label": "getConstInfoRec",
+  {"textEdit": null,
+   "label": "getConstInfoRec",
    "kind": 3,
+   "documentation": null,
    "detail":
    "[inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m RecursorVal"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/compHeader.lean.expected.out b/tests/lean/interactive/compHeader.lean.expected.out
index 3be618a0fc..51cf03f83d 100644
--- a/tests/lean/interactive/compHeader.lean.expected.out
+++ b/tests/lean/interactive/compHeader.lean.expected.out
@@ -1,6 +1,14 @@
 {"textDocument": {"uri": "file://compHeader.lean"},
  "position": {"line": 2, "character": 22}}
 {"items":
- [{"label": "veryLongNam", "kind": 6, "detail": "Sort u_1"},
-  {"label": "veryLongNameForCompletion", "kind": 21, "detail": "Type"}],
+ [{"textEdit": null,
+   "label": "veryLongNam",
+   "kind": 6,
+   "documentation": null,
+   "detail": "Sort u_1"},
+  {"textEdit": null,
+   "label": "veryLongNameForCompletion",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Type"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/compNamespace.lean.expected.out b/tests/lean/interactive/compNamespace.lean.expected.out
index 78a759c773..7e079ad944 100644
--- a/tests/lean/interactive/compNamespace.lean.expected.out
+++ b/tests/lean/interactive/compNamespace.lean.expected.out
@@ -1,21 +1,45 @@
 {"textDocument": {"uri": "file://compNamespace.lean"},
  "position": {"line": 5, "character": 12}}
-{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}],
+{"items":
+ [{"textEdit": null,
+   "label": "LongNamespaceExample",
+   "kind": 9,
+   "documentation": null,
+   "detail": "namespace"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://compNamespace.lean"},
  "position": {"line": 9, "character": 12}}
-{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}],
+{"items":
+ [{"textEdit": null,
+   "label": "LongNamespaceExample",
+   "kind": 9,
+   "documentation": null,
+   "detail": "namespace"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://compNamespace.lean"},
  "position": {"line": 13, "character": 11}}
-{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}],
+{"items":
+ [{"textEdit": null,
+   "label": "LongNamespaceExample",
+   "kind": 9,
+   "documentation": null,
+   "detail": "namespace"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://compNamespace.lean"},
  "position": {"line": 16, "character": 16}}
 {"items":
- [{"label": "Foo.LongNamespaceExample", "kind": 9, "detail": "namespace"}],
+ [{"textEdit": null,
+   "label": "Foo.LongNamespaceExample",
+   "kind": 9,
+   "documentation": null,
+   "detail": "namespace"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://compNamespace.lean"},
  "position": {"line": 20, "character": 12}}
-{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}],
+{"items":
+ [{"textEdit": null,
+   "label": "LongNamespaceExample",
+   "kind": 9,
+   "documentation": null,
+   "detail": "namespace"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out
index 28419bfb88..4d7ea17d8a 100644
--- a/tests/lean/interactive/completion.lean.expected.out
+++ b/tests/lean/interactive/completion.lean.expected.out
@@ -1,16 +1,36 @@
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 3, "character": 22}}
-{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}],
+{"items":
+ [{"textEdit": null,
+   "label": "foo",
+   "kind": 5,
+   "documentation": null,
+   "detail": "Foo → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 5, "character": 23}}
-{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}],
+{"items":
+ [{"textEdit": null,
+   "label": "foo",
+   "kind": 5,
+   "documentation": null,
+   "detail": "Foo → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 7, "character": 28}}
-{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}],
+{"items":
+ [{"textEdit": null,
+   "label": "foo",
+   "kind": 5,
+   "documentation": null,
+   "detail": "Foo → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
  "position": {"line": 9, "character": 29}}
-{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}],
+{"items":
+ [{"textEdit": null,
+   "label": "foo",
+   "kind": 5,
+   "documentation": null,
+   "detail": "Foo → Nat"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out
index f721ab7c71..fc7eedc6b3 100644
--- a/tests/lean/interactive/completion2.lean.expected.out
+++ b/tests/lean/interactive/completion2.lean.expected.out
@@ -1,31 +1,91 @@
 {"textDocument": {"uri": "file://completion2.lean"},
  "position": {"line": 19, "character": 10}}
 {"items":
- [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"},
-  {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
-  {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"},
-  {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}],
+ [{"textEdit": null,
+   "label": "ex2",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + 2 ≤ b + 2"},
+  {"textEdit": null,
+   "label": "ex3",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
+  {"textEdit": null,
+   "label": "ax1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a - a ≤ b - b"},
+  {"textEdit": null,
+   "label": "ex1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + a ≤ b + b"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion2.lean"},
  "position": {"line": 25, "character": 6}}
 {"items":
- [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"},
-  {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
-  {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"},
-  {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}],
+ [{"textEdit": null,
+   "label": "ex2",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + 2 ≤ b + 2"},
+  {"textEdit": null,
+   "label": "ex3",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
+  {"textEdit": null,
+   "label": "ax1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a - a ≤ b - b"},
+  {"textEdit": null,
+   "label": "ex1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + a ≤ b + b"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion2.lean"},
  "position": {"line": 30, "character": 21}}
 {"items":
- [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"},
-  {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
-  {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"},
-  {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}],
+ [{"textEdit": null,
+   "label": "ex2",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + 2 ≤ b + 2"},
+  {"textEdit": null,
+   "label": "ex3",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
+  {"textEdit": null,
+   "label": "ax1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a - a ≤ b - b"},
+  {"textEdit": null,
+   "label": "ex1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + a ≤ b + b"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion2.lean"},
  "position": {"line": 37, "character": 22}}
 {"items":
- [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"},
-  {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
-  {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}],
+ [{"textEdit": null,
+   "label": "ex2",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + 2 ≤ b + 2"},
+  {"textEdit": null,
+   "label": "ex3",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"},
+  {"textEdit": null,
+   "label": "ex1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "a ≤ b → a + a ≤ b + b"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out
index 48ba7a29a1..2b184c48af 100644
--- a/tests/lean/interactive/completion3.lean.expected.out
+++ b/tests/lean/interactive/completion3.lean.expected.out
@@ -1,28 +1,76 @@
 {"textDocument": {"uri": "file://completion3.lean"},
  "position": {"line": 7, "character": 9}}
 {"items":
- [{"label": "b", "kind": 5, "detail": "S → Bool"},
-  {"label": "x", "kind": 5, "detail": "S → Nat"},
-  {"label": "y", "kind": 5, "detail": "S → String"}],
+ [{"textEdit": null,
+   "label": "b",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool"},
+  {"textEdit": null,
+   "label": "x",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "y",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion3.lean"},
  "position": {"line": 12, "character": 5}}
 {"items":
- [{"label": "b", "kind": 5, "detail": "S → Bool"},
-  {"label": "x", "kind": 5, "detail": "S → Nat"},
-  {"label": "y", "kind": 5, "detail": "S → String"}],
+ [{"textEdit": null,
+   "label": "b",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool"},
+  {"textEdit": null,
+   "label": "x",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "y",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion3.lean"},
  "position": {"line": 16, "character": 5}}
 {"items":
- [{"label": "b", "kind": 5, "detail": "S → Bool"},
-  {"label": "x", "kind": 5, "detail": "S → Nat"},
-  {"label": "y", "kind": 5, "detail": "S → String"}],
+ [{"textEdit": null,
+   "label": "b",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool"},
+  {"textEdit": null,
+   "label": "x",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "y",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion3.lean"},
  "position": {"line": 20, "character": 5}}
 {"items":
- [{"label": "x", "kind": 5, "detail": "S → Nat"},
-  {"label": "b", "kind": 5, "detail": "S → Bool"},
-  {"label": "y", "kind": 5, "detail": "S → String"}],
+ [{"textEdit": null,
+   "label": "x",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "b",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool"},
+  {"textEdit": null,
+   "label": "y",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion4.lean.expected.out b/tests/lean/interactive/completion4.lean.expected.out
index 88b2e8c18d..a04803c7df 100644
--- a/tests/lean/interactive/completion4.lean.expected.out
+++ b/tests/lean/interactive/completion4.lean.expected.out
@@ -1,28 +1,76 @@
 {"textDocument": {"uri": "file://completion4.lean"},
  "position": {"line": 7, "character": 4}}
 {"items":
- [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"},
-  {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"},
-  {"label": "pred", "kind": 5, "detail": "S → String → Bool"}],
+ [{"textEdit": null,
+   "label": "fn1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat → IO Unit"},
+  {"textEdit": null,
+   "label": "fn2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool → IO Unit"},
+  {"textEdit": null,
+   "label": "pred",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion4.lean"},
  "position": {"line": 11, "character": 10}}
 {"items":
- [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"},
-  {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"},
-  {"label": "pred", "kind": 5, "detail": "S → String → Bool"}],
+ [{"textEdit": null,
+   "label": "fn1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat → IO Unit"},
+  {"textEdit": null,
+   "label": "fn2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool → IO Unit"},
+  {"textEdit": null,
+   "label": "pred",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion4.lean"},
  "position": {"line": 16, "character": 11}}
 {"items":
- [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"},
-  {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"},
-  {"label": "pred", "kind": 5, "detail": "S → String → Bool"}],
+ [{"textEdit": null,
+   "label": "fn1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat → IO Unit"},
+  {"textEdit": null,
+   "label": "fn2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool → IO Unit"},
+  {"textEdit": null,
+   "label": "pred",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion4.lean"},
  "position": {"line": 20, "character": 21}}
 {"items":
- [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"},
-  {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"},
-  {"label": "pred", "kind": 5, "detail": "S → String → Bool"}],
+ [{"textEdit": null,
+   "label": "fn1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat → IO Unit"},
+  {"textEdit": null,
+   "label": "fn2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool → IO Unit"},
+  {"textEdit": null,
+   "label": "pred",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String → Bool"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out
index 38d270ac56..ad2ae5bb86 100644
--- a/tests/lean/interactive/completion5.lean.expected.out
+++ b/tests/lean/interactive/completion5.lean.expected.out
@@ -1,7 +1,19 @@
 {"textDocument": {"uri": "file://completion5.lean"},
  "position": {"line": 9, "character": 15}}
 {"items":
- [{"label": "b1", "kind": 5, "detail": "C → String"},
-  {"label": "f1", "kind": 5, "detail": "C → Nat"},
-  {"label": "f2", "kind": 5, "detail": "C → Bool"}],
+ [{"textEdit": null,
+   "label": "b1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → String"},
+  {"textEdit": null,
+   "label": "f1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Nat"},
+  {"textEdit": null,
+   "label": "f2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Bool"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion6.lean.expected.out b/tests/lean/interactive/completion6.lean.expected.out
index d3976fb926..da6655961c 100644
--- a/tests/lean/interactive/completion6.lean.expected.out
+++ b/tests/lean/interactive/completion6.lean.expected.out
@@ -1,19 +1,63 @@
 {"textDocument": {"uri": "file://completion6.lean"},
  "position": {"line": 12, "character": 15}}
 {"items":
- [{"label": "b1", "kind": 5, "detail": "C → String"},
-  {"label": "f1", "kind": 5, "detail": "C → Nat"},
-  {"label": "f2", "kind": 5, "detail": "C → Bool"},
-  {"label": "f3", "kind": 5, "detail": "D → Bool"},
-  {"label": "toC", "kind": 5, "detail": "D → C"}],
+ [{"textEdit": null,
+   "label": "b1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → String"},
+  {"textEdit": null,
+   "label": "f1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Nat"},
+  {"textEdit": null,
+   "label": "f2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Bool"},
+  {"textEdit": null,
+   "label": "f3",
+   "kind": 5,
+   "documentation": null,
+   "detail": "D → Bool"},
+  {"textEdit": null,
+   "label": "toC",
+   "kind": 5,
+   "documentation": null,
+   "detail": "D → C"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion6.lean"},
  "position": {"line": 21, "character": 4}}
 {"items":
- [{"label": "b1", "kind": 5, "detail": "C → String"},
-  {"label": "doubleF1", "kind": 3, "detail": "E → Nat"},
-  {"label": "f1", "kind": 5, "detail": "C → Nat"},
-  {"label": "f2", "kind": 5, "detail": "C → Bool"},
-  {"label": "f3", "kind": 5, "detail": "D → Bool"},
-  {"label": "toC", "kind": 5, "detail": "D → C"}],
+ [{"textEdit": null,
+   "label": "b1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → String"},
+  {"textEdit": null,
+   "label": "doubleF1",
+   "kind": 3,
+   "documentation": null,
+   "detail": "E → Nat"},
+  {"textEdit": null,
+   "label": "f1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Nat"},
+  {"textEdit": null,
+   "label": "f2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Bool"},
+  {"textEdit": null,
+   "label": "f3",
+   "kind": 5,
+   "documentation": null,
+   "detail": "D → Bool"},
+  {"textEdit": null,
+   "label": "toC",
+   "kind": 5,
+   "documentation": null,
+   "detail": "D → C"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out
index 188f4363d6..d98030937e 100644
--- a/tests/lean/interactive/completion7.lean.expected.out
+++ b/tests/lean/interactive/completion7.lean.expected.out
@@ -1,58 +1,154 @@
 {"textDocument": {"uri": "file://completion7.lean"},
  "position": {"line": 0, "character": 10}}
 {"items":
- [{"label": "And", "kind": 22, "detail": "Prop → Prop → Prop"},
-  {"label": "AndOp", "kind": 7, "detail": "Type u → Type u"},
-  {"label": "AndThen", "kind": 7, "detail": "Type u → Type u"},
-  {"label": "and", "kind": 3, "detail": "Bool → Bool → Bool"},
-  {"label": "andM",
+ [{"textEdit": null,
+   "label": "And",
+   "kind": 22,
+   "documentation": null,
+   "detail": "Prop → Prop → Prop"},
+  {"textEdit": null,
+   "label": "AndOp",
+   "kind": 7,
+   "documentation": null,
+   "detail": "Type u → Type u"},
+  {"textEdit": null,
+   "label": "AndThen",
+   "kind": 7,
+   "documentation": null,
+   "detail": "Type u → Type u"},
+  {"textEdit": null,
+   "label": "and",
    "kind": 3,
+   "documentation": null,
+   "detail": "Bool → Bool → Bool"},
+  {"textEdit": null,
+   "label": "andM",
+   "kind": 3,
+   "documentation": null,
    "detail": "[inst : Monad m] → [inst : ToBool β] → m β → m β → m β"},
-  {"label": "and_false",
+  {"textEdit": null,
+   "label": "and_false",
    "kind": 3,
+   "documentation": null,
    "detail": "∀ (p : Prop), (p ∧ False) = False"},
-  {"label": "and_self", "kind": 3, "detail": "∀ (p : Prop), (p ∧ p) = p"},
-  {"label": "and_true", "kind": 3, "detail": "∀ (p : Prop), (p ∧ True) = p"},
-  {"label": "Append", "kind": 7, "detail": "Type u → Type u"},
-  {"label": "HAnd",
-   "kind": 7,
-   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "HAndThen",
-   "kind": 7,
-   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "false_and",
+  {"textEdit": null,
+   "label": "and_self",
    "kind": 3,
+   "documentation": null,
+   "detail": "∀ (p : Prop), (p ∧ p) = p"},
+  {"textEdit": null,
+   "label": "and_true",
+   "kind": 3,
+   "documentation": null,
+   "detail": "∀ (p : Prop), (p ∧ True) = p"},
+  {"textEdit": null,
+   "label": "Append",
+   "kind": 7,
+   "documentation": null,
+   "detail": "Type u → Type u"},
+  {"textEdit": null,
+   "label": "HAnd",
+   "kind": 7,
+   "documentation": null,
+   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
+  {"textEdit": null,
+   "label": "HAndThen",
+   "kind": 7,
+   "documentation": null,
+   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
+  {"textEdit": null,
+   "label": "false_and",
+   "kind": 3,
+   "documentation": null,
    "detail": "∀ (p : Prop), (False ∧ p) = False"},
-  {"label": "instAndOpUInt16", "kind": 21, "detail": "AndOp UInt16"},
-  {"label": "instAndOpUInt32", "kind": 21, "detail": "AndOp UInt32"},
-  {"label": "instAndOpUInt64", "kind": 21, "detail": "AndOp UInt64"},
-  {"label": "instAndOpUInt8", "kind": 21, "detail": "AndOp UInt8"},
-  {"label": "instAndOpUSize", "kind": 21, "detail": "AndOp USize"},
-  {"label": "strictAnd", "kind": 3, "detail": "Bool → Bool → Bool"},
-  {"label": "true_and", "kind": 3, "detail": "∀ (p : Prop), (True ∧ p) = p"},
-  {"label": "instDecidableAnd",
+  {"textEdit": null,
+   "label": "instAndOpUInt16",
+   "kind": 21,
+   "documentation": null,
+   "detail": "AndOp UInt16"},
+  {"textEdit": null,
+   "label": "instAndOpUInt32",
+   "kind": 21,
+   "documentation": null,
+   "detail": "AndOp UInt32"},
+  {"textEdit": null,
+   "label": "instAndOpUInt64",
+   "kind": 21,
+   "documentation": null,
+   "detail": "AndOp UInt64"},
+  {"textEdit": null,
+   "label": "instAndOpUInt8",
+   "kind": 21,
+   "documentation": null,
+   "detail": "AndOp UInt8"},
+  {"textEdit": null,
+   "label": "instAndOpUSize",
+   "kind": 21,
+   "documentation": null,
+   "detail": "AndOp USize"},
+  {"textEdit": null,
+   "label": "strictAnd",
    "kind": 3,
+   "documentation": null,
+   "detail": "Bool → Bool → Bool"},
+  {"textEdit": null,
+   "label": "true_and",
+   "kind": 3,
+   "documentation": null,
+   "detail": "∀ (p : Prop), (True ∧ p) = p"},
+  {"textEdit": null,
+   "label": "instDecidableAnd",
+   "kind": 3,
+   "documentation": null,
    "detail": "[dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)"},
-  {"label": "instHAnd", "kind": 3, "detail": "[inst : AndOp α] → HAnd α α α"},
-  {"label": "instHAndThen",
+  {"textEdit": null,
+   "label": "instHAnd",
    "kind": 3,
+   "documentation": null,
+   "detail": "[inst : AndOp α] → HAnd α α α"},
+  {"textEdit": null,
+   "label": "instHAndThen",
+   "kind": 3,
+   "documentation": null,
    "detail": "[inst : AndThen α] → HAndThen α α α"},
-  {"label": "compareOfLessAndEq",
+  {"textEdit": null,
+   "label": "compareOfLessAndEq",
    "kind": 3,
+   "documentation": null,
    "detail":
    "(x y : α) → [inst : LT α] → [inst : Decidable (x < y)] → [inst : DecidableEq α] → Ordering"},
-  {"label": "iff_iff_implies_and_implies",
+  {"textEdit": null,
+   "label": "iff_iff_implies_and_implies",
    "kind": 3,
+   "documentation": null,
    "detail": "∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)"},
-  {"label": "HAppend",
+  {"textEdit": null,
+   "label": "HAppend",
    "kind": 7,
+   "documentation": null,
    "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "instAppendSubarray", "kind": 3, "detail": "Append (Subarray α)"}],
+  {"textEdit": null,
+   "label": "instAppendSubarray",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Append (Subarray α)"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion7.lean"},
  "position": {"line": 2, "character": 11}}
 {"items":
- [{"label": "intro", "kind": 4, "detail": "a → b → a ∧ b"},
-  {"label": "left", "kind": 5, "detail": "a ∧ b → a"},
-  {"label": "right", "kind": 5, "detail": "a ∧ b → b"}],
+ [{"textEdit": null,
+   "label": "intro",
+   "kind": 4,
+   "documentation": null,
+   "detail": "a → b → a ∧ b"},
+  {"textEdit": null,
+   "label": "left",
+   "kind": 5,
+   "documentation": null,
+   "detail": "a ∧ b → a"},
+  {"textEdit": null,
+   "label": "right",
+   "kind": 5,
+   "documentation": null,
+   "detail": "a ∧ b → b"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completionAtPrint.lean.expected.out b/tests/lean/interactive/completionAtPrint.lean.expected.out
index edf3bd6a25..a3d785a906 100644
--- a/tests/lean/interactive/completionAtPrint.lean.expected.out
+++ b/tests/lean/interactive/completionAtPrint.lean.expected.out
@@ -1,10 +1,13 @@
 {"textDocument": {"uri": "file://completionAtPrint.lean"},
  "position": {"line": 2, "character": 25}}
 {"items":
- [{"label": "find?",
+ [{"textEdit": null,
+   "label": "find?",
    "kind": 3,
+   "documentation": null,
    "detail": "Lean.Environment → Lean.Name → Option Lean.ConstantInfo"},
-  {"label": "freeRegions",
+  {"textEdit": null,
+   "label": "freeRegions",
    "kind": 3,
    "documentation":
    {"value":
diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out
index 02fa3fdd22..28aaedd797 100644
--- a/tests/lean/interactive/completionDocString.lean.expected.out
+++ b/tests/lean/interactive/completionDocString.lean.expected.out
@@ -1,13 +1,16 @@
 {"textDocument": {"uri": "file://completionDocString.lean"},
  "position": {"line": 0, "character": 20}}
 {"items":
- [{"label": "insertAt",
+ [{"textEdit": null,
+   "label": "insertAt",
    "kind": 3,
    "documentation":
    {"value": "Insert element `a` at position `i`.\n  Pre: `i < as.size` ",
     "kind": "markdown"},
    "detail": "Array α → Nat → α → Array α"},
-  {"label": "insertAtAux",
+  {"textEdit": null,
+   "label": "insertAtAux",
    "kind": 3,
+   "documentation": null,
    "detail": "Nat → Array α → Nat → Array α"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completionEOF.lean.expected.out b/tests/lean/interactive/completionEOF.lean.expected.out
index db1c3bdafa..3828e2dd59 100644
--- a/tests/lean/interactive/completionEOF.lean.expected.out
+++ b/tests/lean/interactive/completionEOF.lean.expected.out
@@ -1,4 +1,9 @@
 {"textDocument": {"uri": "file://completionEOF.lean"},
  "position": {"line": 8, "character": 9}}
-{"items": [{"label": "And", "kind": 21, "detail": "Type"}],
+{"items":
+ [{"textEdit": null,
+   "label": "And",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Type"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completionIStr.lean.expected.out b/tests/lean/interactive/completionIStr.lean.expected.out
index 2735770873..f9808e4f6d 100644
--- a/tests/lean/interactive/completionIStr.lean.expected.out
+++ b/tests/lean/interactive/completionIStr.lean.expected.out
@@ -1,7 +1,19 @@
 {"textDocument": {"uri": "file://completionIStr.lean"},
  "position": {"line": 5, "character": 34}}
 {"items":
- [{"label": "b1", "kind": 5, "detail": "C → String"},
-  {"label": "f1", "kind": 5, "detail": "C → Nat"},
-  {"label": "f2", "kind": 5, "detail": "C → Bool"}],
+ [{"textEdit": null,
+   "label": "b1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → String"},
+  {"textEdit": null,
+   "label": "f1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Nat"},
+  {"textEdit": null,
+   "label": "f2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Bool"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out
index 409061b031..1547d0606c 100644
--- a/tests/lean/interactive/completionOption.lean.expected.out
+++ b/tests/lean/interactive/completionOption.lean.expected.out
@@ -11,6 +11,7 @@
      "end": {"line": 1, "character": 13}}},
    "label": "format.indent",
    "kind": 10,
+   "documentation": null,
    "detail": "(2), indentation"},
   {"textEdit":
    {"replace":
@@ -22,6 +23,7 @@
      "end": {"line": 1, "character": 13}}},
    "label": "format.unicode",
    "kind": 10,
+   "documentation": null,
    "detail": "(true), unicode characters"},
   {"textEdit":
    {"replace":
@@ -33,6 +35,7 @@
      "end": {"line": 1, "character": 13}}},
    "label": "format.width",
    "kind": 10,
+   "documentation": null,
    "detail": "(120), indentation"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
@@ -48,6 +51,7 @@
      "end": {"line": 4, "character": 17}}},
    "label": "format.indent",
    "kind": 10,
+   "documentation": null,
    "detail": "(2), indentation"},
   {"textEdit":
    {"replace":
@@ -59,6 +63,7 @@
      "end": {"line": 4, "character": 17}}},
    "label": "format.unicode",
    "kind": 10,
+   "documentation": null,
    "detail": "(true), unicode characters"},
   {"textEdit":
    {"replace":
@@ -70,6 +75,7 @@
      "end": {"line": 4, "character": 17}}},
    "label": "format.width",
    "kind": 10,
+   "documentation": null,
    "detail": "(120), indentation"},
   {"textEdit":
    {"replace":
@@ -81,6 +87,7 @@
      "end": {"line": 4, "character": 17}}},
    "label": "trace.PrettyPrinter.format",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"}],
  "isIncomplete": true}
@@ -97,6 +104,7 @@
      "end": {"line": 7, "character": 20}}},
    "label": "format.indent",
    "kind": 10,
+   "documentation": null,
    "detail": "(2), indentation"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
@@ -112,6 +120,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.PrettyPrinter",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -124,6 +133,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.PrettyPrinter.delab",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -136,6 +146,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.PrettyPrinter.format",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -148,6 +159,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.PrettyPrinter.parenthesize",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -160,6 +172,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.pp.analyze",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -172,6 +185,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.pp.analyze.annotate",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -184,6 +198,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.pp.analyze.error",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -196,6 +211,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.pp.analyze.tryUnify",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -208,6 +224,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.Elab.postpone",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -220,6 +237,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.Meta.IndPredBelow",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -232,6 +250,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.Meta.IndPredBelow.match",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -244,6 +263,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.Meta.synthPending",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -256,6 +276,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.compiler.ir.push_proj",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), (trace) enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -268,6 +289,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.compiler.lambda_pure",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), (trace) enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -280,6 +302,7 @@
      "end": {"line": 10, "character": 18}}},
    "label": "trace.Meta.isLevelDefEq.postponed",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"}],
  "isIncomplete": true}
@@ -296,6 +319,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.pp.analyze",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -308,6 +332,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.pp.analyze.annotate",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -320,6 +345,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.pp.analyze.error",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -332,6 +358,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.pp.analyze.tryUnify",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -344,6 +371,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.PrettyPrinter",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -356,6 +384,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.PrettyPrinter.delab",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -368,6 +397,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.PrettyPrinter.format",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -380,6 +410,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.PrettyPrinter.parenthesize",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -392,6 +423,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.compiler.ir.push_proj",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), (trace) enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -404,6 +436,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.Elab.postpone",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -416,6 +449,7 @@
      "end": {"line": 13, "character": 19}}},
    "label": "trace.Meta.isLevelDefEq.postponed",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"}],
  "isIncomplete": true}
@@ -432,6 +466,7 @@
      "end": {"line": 16, "character": 23}}},
    "label": "trace.pp.analyze",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -444,6 +479,7 @@
      "end": {"line": 16, "character": 23}}},
    "label": "trace.pp.analyze.annotate",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -456,6 +492,7 @@
      "end": {"line": 16, "character": 23}}},
    "label": "trace.pp.analyze.error",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -468,6 +505,7 @@
      "end": {"line": 16, "character": 23}}},
    "label": "trace.pp.analyze.tryUnify",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"}],
  "isIncomplete": true}
@@ -484,6 +522,7 @@
      "end": {"line": 19, "character": 27}}},
    "label": "trace.pp.analyze",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -496,6 +535,7 @@
      "end": {"line": 19, "character": 27}}},
    "label": "trace.pp.analyze.annotate",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -508,6 +548,7 @@
      "end": {"line": 19, "character": 27}}},
    "label": "trace.pp.analyze.error",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"},
   {"textEdit":
@@ -520,6 +561,7 @@
      "end": {"line": 19, "character": 27}}},
    "label": "trace.pp.analyze.tryUnify",
    "kind": 10,
+   "documentation": null,
    "detail":
    "(false), enable/disable tracing for the given module and submodules"}],
  "isIncomplete": true}
@@ -536,6 +578,7 @@
      "end": {"line": 22, "character": 13}}},
    "label": "format.indent",
    "kind": 10,
+   "documentation": null,
    "detail": "(2), indentation"},
   {"textEdit":
    {"replace":
@@ -547,6 +590,7 @@
      "end": {"line": 22, "character": 13}}},
    "label": "format.unicode",
    "kind": 10,
+   "documentation": null,
    "detail": "(true), unicode characters"},
   {"textEdit":
    {"replace":
@@ -558,6 +602,7 @@
      "end": {"line": 22, "character": 13}}},
    "label": "format.width",
    "kind": 10,
+   "documentation": null,
    "detail": "(120), indentation"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
@@ -573,6 +618,7 @@
      "end": {"line": 25, "character": 18}}},
    "label": "format.indent",
    "kind": 10,
+   "documentation": null,
    "detail": "(2), indentation"},
   {"textEdit":
    {"replace":
@@ -584,6 +630,7 @@
      "end": {"line": 25, "character": 18}}},
    "label": "format.unicode",
    "kind": 10,
+   "documentation": null,
    "detail": "(true), unicode characters"},
   {"textEdit":
    {"replace":
@@ -595,5 +642,6 @@
      "end": {"line": 25, "character": 18}}},
    "label": "format.width",
    "kind": 10,
+   "documentation": null,
    "detail": "(120), indentation"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completionPrefixIssue.lean.expected.out b/tests/lean/interactive/completionPrefixIssue.lean.expected.out
index 4d4d4bff94..dc13da6e6a 100644
--- a/tests/lean/interactive/completionPrefixIssue.lean.expected.out
+++ b/tests/lean/interactive/completionPrefixIssue.lean.expected.out
@@ -1,8 +1,14 @@
 {"textDocument": {"uri": "file://completionPrefixIssue.lean"},
  "position": {"line": 1, "character": 64}}
 {"items":
- [{"label": "veryLongDefinitionName", "kind": 6, "detail": "Nat"},
-  {"label": "veryLongDefinitionNameVeryLongDefinitionName",
+ [{"textEdit": null,
+   "label": "veryLongDefinitionName",
+   "kind": 6,
+   "documentation": null,
+   "detail": "Nat"},
+  {"textEdit": null,
+   "label": "veryLongDefinitionNameVeryLongDefinitionName",
    "kind": 21,
+   "documentation": null,
    "detail": "Nat"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out
index c0cda68c20..8e46b323b1 100644
--- a/tests/lean/interactive/completionPrv.lean.expected.out
+++ b/tests/lean/interactive/completionPrv.lean.expected.out
@@ -1,25 +1,56 @@
 {"textDocument": {"uri": "file://completionPrv.lean"},
  "position": {"line": 2, "character": 11}}
-{"items": [{"label": "blaBlaBoo", "kind": 21, "detail": "Nat"}],
+{"items":
+ [{"textEdit": null,
+   "label": "blaBlaBoo",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionPrv.lean"},
  "position": {"line": 9, "character": 11}}
 {"items":
- [{"label": "booBoo", "kind": 21, "detail": "Nat"},
-  {"label": "instToBoolBool", "kind": 21, "detail": "ToBool Bool"},
-  {"label": "instLawfulBEqBoolInstBEqInstDecidableEqBool",
+ [{"textEdit": null,
+   "label": "booBoo",
    "kind": 21,
+   "documentation": null,
+   "detail": "Nat"},
+  {"textEdit": null,
+   "label": "instToBoolBool",
+   "kind": 21,
+   "documentation": null,
+   "detail": "ToBool Bool"},
+  {"textEdit": null,
+   "label": "instLawfulBEqBoolInstBEqInstDecidableEqBool",
+   "kind": 21,
+   "documentation": null,
    "detail": "LawfulBEq Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionPrv.lean"},
  "position": {"line": 21, "character": 5}}
 {"items":
- [{"label": "field1", "kind": 5, "detail": "S → Nat"},
-  {"label": "getInc", "kind": 3, "detail": "S → Nat"}],
+ [{"textEdit": null,
+   "label": "field1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "getInc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "S → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionPrv.lean"},
  "position": {"line": 25, "character": 4}}
 {"items":
- [{"label": "field1", "kind": 5, "detail": "S → Nat"},
-  {"label": "getInc", "kind": 3, "detail": "S → Nat"}],
+ [{"textEdit": null,
+   "label": "field1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "getInc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "S → Nat"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/editAfterError.lean.expected.out b/tests/lean/interactive/editAfterError.lean.expected.out
index 3ad143e86c..78b021e507 100644
--- a/tests/lean/interactive/editAfterError.lean.expected.out
+++ b/tests/lean/interactive/editAfterError.lean.expected.out
@@ -7,54 +7,69 @@
 {"version": 2,
  "uri": "file://editAfterError.lean",
  "diagnostics":
- [{"source": "Lean 4",
+ [{"tags": null,
+   "source": "Lean 4",
    "severity": 1,
+   "relatedInformation": null,
    "range":
    {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
    "message": "unknown identifier 'tru'",
    "fullRange":
-   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}},
-  {"source": "Lean 4",
+   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
+   "code": null},
+  {"tags": null,
+   "source": "Lean 4",
    "severity": 1,
+   "relatedInformation": null,
    "range":
    {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
    "message": "unknown identifier 'fals'",
    "fullRange":
-   {"start": {"line": 1, "character": 7},
-    "end": {"line": 1, "character": 11}}}]}
+   {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
+   "code": null}]}
 {"version": 2,
  "uri": "file://editAfterError.lean",
  "diagnostics":
- [{"source": "Lean 4",
+ [{"tags": null,
+   "source": "Lean 4",
    "severity": 1,
+   "relatedInformation": null,
    "range":
    {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
    "message": "unknown identifier 'tru'",
    "fullRange":
-   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}},
-  {"source": "Lean 4",
+   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
+   "code": null},
+  {"tags": null,
+   "source": "Lean 4",
    "severity": 1,
+   "relatedInformation": null,
    "range":
    {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
    "message": "unknown identifier 'fals'",
    "fullRange":
-   {"start": {"line": 1, "character": 7},
-    "end": {"line": 1, "character": 11}}}]}
+   {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
+   "code": null}]}
 {"version": 2,
  "uri": "file://editAfterError.lean",
  "diagnostics":
- [{"source": "Lean 4",
+ [{"tags": null,
+   "source": "Lean 4",
    "severity": 1,
+   "relatedInformation": null,
    "range":
    {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
    "message": "unknown identifier 'tru'",
    "fullRange":
-   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}},
-  {"source": "Lean 4",
+   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
+   "code": null},
+  {"tags": null,
+   "source": "Lean 4",
    "severity": 1,
+   "relatedInformation": null,
    "range":
    {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
    "message": "unknown identifier 'fals'",
    "fullRange":
-   {"start": {"line": 1, "character": 7},
-    "end": {"line": 1, "character": 11}}}]}
+   {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
+   "code": null}]}
diff --git a/tests/lean/interactive/editCompletion.lean.expected.out b/tests/lean/interactive/editCompletion.lean.expected.out
index d80fe93880..213869d881 100644
--- a/tests/lean/interactive/editCompletion.lean.expected.out
+++ b/tests/lean/interactive/editCompletion.lean.expected.out
@@ -6,5 +6,10 @@
     "end": {"line": 3, "character": 22}}}]}
 {"textDocument": {"uri": "file://editCompletion.lean"},
  "position": {"line": 3, "character": 22}}
-{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}],
+{"items":
+ [{"textEdit": null,
+   "label": "foo",
+   "kind": 5,
+   "documentation": null,
+   "detail": "Foo → Nat"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/inWordCompletion.lean.expected.out b/tests/lean/interactive/inWordCompletion.lean.expected.out
index 45517b1676..dc040961e0 100644
--- a/tests/lean/interactive/inWordCompletion.lean.expected.out
+++ b/tests/lean/interactive/inWordCompletion.lean.expected.out
@@ -1,14 +1,38 @@
 {"textDocument": {"uri": "file://inWordCompletion.lean"},
  "position": {"line": 5, "character": 10}}
 {"items":
- [{"label": "gfabc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfacc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfadc", "kind": 3, "detail": "Nat → Nat"}],
+ [{"textEdit": null,
+   "label": "gfabc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"},
+  {"textEdit": null,
+   "label": "gfacc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"},
+  {"textEdit": null,
+   "label": "gfadc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://inWordCompletion.lean"},
  "position": {"line": 13, "character": 14}}
 {"items":
- [{"label": "gfabc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfacc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfadc", "kind": 3, "detail": "Nat → Nat"}],
+ [{"textEdit": null,
+   "label": "gfabc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"},
+  {"textEdit": null,
+   "label": "gfacc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"},
+  {"textEdit": null,
+   "label": "gfadc",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/internalNamesIssue.lean.expected.out b/tests/lean/interactive/internalNamesIssue.lean.expected.out
index 2a72302a74..98e7d9d4c4 100644
--- a/tests/lean/interactive/internalNamesIssue.lean.expected.out
+++ b/tests/lean/interactive/internalNamesIssue.lean.expected.out
@@ -1,6 +1,14 @@
 {"textDocument": {"uri": "file://internalNamesIssue.lean"},
  "position": {"line": 9, "character": 11}}
 {"items":
- [{"label": "bla", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "foo", "kind": 3, "detail": "Nat → Nat"}],
+ [{"textEdit": null,
+   "label": "bla",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"},
+  {"textEdit": null,
+   "label": "foo",
+   "kind": 3,
+   "documentation": null,
+   "detail": "Nat → Nat"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out
index 11123ebbd7..853c7634f3 100644
--- a/tests/lean/interactive/keywordCompletion.lean.expected.out
+++ b/tests/lean/interactive/keywordCompletion.lean.expected.out
@@ -1,19 +1,49 @@
 {"textDocument": {"uri": "file://keywordCompletion.lean"},
  "position": {"line": 4, "character": 16}}
 {"items":
- [{"label": "register_string", "kind": 14, "detail": "keyword"},
-  {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"}],
+ [{"textEdit": null,
+   "label": "register_string",
+   "kind": 14,
+   "documentation": null,
+   "detail": "keyword"},
+  {"textEdit": null,
+   "label": "termRegister_string_",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Lean.ParserDescr"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://keywordCompletion.lean"},
  "position": {"line": 7, "character": 10}}
 {"items":
- [{"label": "register_string", "kind": 14, "detail": "keyword"},
-  {"label": "regular", "kind": 21, "detail": "Nat"},
-  {"label": "recSubsingleton",
+ [{"textEdit": null,
+   "label": "register_string",
+   "kind": 14,
+   "documentation": null,
+   "detail": "keyword"},
+  {"textEdit": null,
+   "label": "regular",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Nat"},
+  {"textEdit": null,
+   "label": "recSubsingleton",
    "kind": 3,
+   "documentation": null,
    "detail":
    "∀ [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)]\n  [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)], Subsingleton (Decidable.casesOn h h₂ h₁)"},
-  {"label": "reprArg", "kind": 3, "detail": "[inst : Repr α] → α → Std.Format"},
-  {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"},
-  {"label": "instReprStdGen", "kind": 21, "detail": "Repr StdGen"}],
+  {"textEdit": null,
+   "label": "reprArg",
+   "kind": 3,
+   "documentation": null,
+   "detail": "[inst : Repr α] → α → Std.Format"},
+  {"textEdit": null,
+   "label": "termRegister_string_",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Lean.ParserDescr"},
+  {"textEdit": null,
+   "label": "instReprStdGen",
+   "kind": 21,
+   "documentation": null,
+   "detail": "Repr StdGen"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/match.lean.expected.out b/tests/lean/interactive/match.lean.expected.out
index 5e4555b01d..f69f441db4 100644
--- a/tests/lean/interactive/match.lean.expected.out
+++ b/tests/lean/interactive/match.lean.expected.out
@@ -1,16 +1,40 @@
 {"textDocument": {"uri": "file://match.lean"},
  "position": {"line": 6, "character": 11}}
 {"items":
- [{"label": "fn1", "kind": 5, "detail": "S → Nat"},
-  {"label": "name", "kind": 5, "detail": "S → String"},
-  {"label": "value", "kind": 5, "detail": "S → Bool"}],
+ [{"textEdit": null,
+   "label": "fn1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "name",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String"},
+  {"textEdit": null,
+   "label": "value",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://match.lean"},
  "position": {"line": 10, "character": 10}}
 {"items":
- [{"label": "fn1", "kind": 5, "detail": "S → Nat"},
-  {"label": "name", "kind": 5, "detail": "S → String"},
-  {"label": "value", "kind": 5, "detail": "S → Bool"}],
+ [{"textEdit": null,
+   "label": "fn1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Nat"},
+  {"textEdit": null,
+   "label": "name",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → String"},
+  {"textEdit": null,
+   "label": "value",
+   "kind": 5,
+   "documentation": null,
+   "detail": "S → Bool"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://match.lean"},
  "position": {"line": 14, "character": 2}}
diff --git a/tests/lean/interactive/matchStxCompletion.lean.expected.out b/tests/lean/interactive/matchStxCompletion.lean.expected.out
index 08c2d30bcc..24853a7919 100644
--- a/tests/lean/interactive/matchStxCompletion.lean.expected.out
+++ b/tests/lean/interactive/matchStxCompletion.lean.expected.out
@@ -1,7 +1,19 @@
 {"textDocument": {"uri": "file://matchStxCompletion.lean"},
  "position": {"line": 8, "character": 9}}
 {"items":
- [{"label": "b1", "kind": 5, "detail": "C → String"},
-  {"label": "f1", "kind": 5, "detail": "C → Nat"},
-  {"label": "f2", "kind": 5, "detail": "C → Bool"}],
+ [{"textEdit": null,
+   "label": "b1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → String"},
+  {"textEdit": null,
+   "label": "f1",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Nat"},
+  {"textEdit": null,
+   "label": "f2",
+   "kind": 5,
+   "documentation": null,
+   "detail": "C → Bool"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/partialNamespace.lean.expected.out b/tests/lean/interactive/partialNamespace.lean.expected.out
index dba4b7af81..e503b5cc76 100644
--- a/tests/lean/interactive/partialNamespace.lean.expected.out
+++ b/tests/lean/interactive/partialNamespace.lean.expected.out
@@ -6,4 +6,5 @@
   {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 9}},
   "name": "[anonymous]",
   "kind": 3,
+  "detail": null,
   "children": []}]