diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 8a809a2c2e..a1ff9a9b01 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki -/ import Lean.DocString import Lean.Elab.InfoTree +import Lean.PrettyPrinter.Delaborator.Options import Lean.Util.Sorry protected structure String.Range where @@ -164,7 +165,8 @@ where match i with | Info.ofTermInfo ti => let tp ← Meta.inferType ti.expr - let eFmt ← Meta.ppExpr ti.expr + let eFmt ← Lean.withOptions (Lean.pp.fullNames.set . true) do + Meta.ppExpr ti.expr let tpFmt ← Meta.ppExpr tp -- try not to show too scary internals let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}" diff --git a/tests/lean/interactive/hoverDot.lean b/tests/lean/interactive/hoverDot.lean index 8b4b9cb0dd..7d442d2a0c 100644 --- a/tests/lean/interactive/hoverDot.lean +++ b/tests/lean/interactive/hoverDot.lean @@ -11,6 +11,7 @@ def Foo.foo : Foo := ⟨10⟩ open Foo #check foo.f₁.succ + --^ textDocument/hover --^ textDocument/hover --^ textDocument/hover #check foo.f₂.succ diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index 7adb2e511f..58d5a0224e 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -3,11 +3,16 @@ {"range": {"start": {"line": 8, "character": 7}, "end": {"line": 8, "character": 14}}, "contents": {"value": "```lean\nFoo.foo : Foo\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file://hoverDot.lean"}, + "position": {"line": 12, "character": 7}} +{"range": + {"start": {"line": 12, "character": 7}, "end": {"line": 12, "character": 10}}, + "contents": {"value": "```lean\nFoo.foo : Foo\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, "position": {"line": 12, "character": 11}} {"range": {"start": {"line": 12, "character": 11}, "end": {"line": 12, "character": 13}}, - "contents": {"value": "```lean\nf₁ : Foo → Nat\n```", "kind": "markdown"}} + "contents": {"value": "```lean\nFoo.f₁ : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, "position": {"line": 12, "character": 14}} {"range": @@ -15,35 +20,35 @@ "contents": {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, - "position": {"line": 15, "character": 11}} + "position": {"line": 16, "character": 11}} {"range": - {"start": {"line": 15, "character": 11}, "end": {"line": 15, "character": 13}}, - "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} + {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 13}}, + "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, - "position": {"line": 15, "character": 14}} + "position": {"line": 16, "character": 14}} {"range": - {"start": {"line": 15, "character": 14}, "end": {"line": 15, "character": 18}}, + {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}}, "contents": {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, - "position": {"line": 18, "character": 13}} + "position": {"line": 19, "character": 13}} {"range": - {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 15}}, - "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} + {"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 15}}, + "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, - "position": {"line": 18, "character": 16}} + "position": {"line": 19, "character": 16}} {"range": - {"start": {"line": 18, "character": 16}, "end": {"line": 18, "character": 20}}, + {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}}, "contents": {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, - "position": {"line": 21, "character": 14}} + "position": {"line": 22, "character": 14}} {"range": - {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 16}}, - "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}} + {"start": {"line": 22, "character": 14}, "end": {"line": 22, "character": 16}}, + "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hoverDot.lean"}, - "position": {"line": 21, "character": 17}} + "position": {"line": 22, "character": 17}} {"range": - {"start": {"line": 21, "character": 17}, "end": {"line": 21, "character": 21}}, + {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}}, "contents": {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}