Show fully-qualified name in hover text

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -60,8 +60,11 @@ def delabSort : Delab := do
 
 def unresolveNameGlobal (n₀ : Name) : DelabM Name := do
   if n₀.hasMacroScopes then return n₀
-  let mut initialNames := #[]
-  if !(← getPPOption getPPFullNames) then initialNames := initialNames ++ getRevAliases (← getEnv) n₀
+  if (← getPPOption getPPFullNames) then
+    match (← resolveGlobalName n₀) with
+      | [(potentialMatch, _)] => if potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀
+      | _ => return n₀ -- if can't resolve, return the original
+  let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     match (← unresolveNameCore initialName) with

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}"

tests/lean/236.lean.expected.out

@@ -1,3 +1,3 @@
 { x := 10, b := true } : Foo
-Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) true : Foo
-{ x := OfNat.ofNat 10, b := true : Foo } : Foo
+Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo
+{ x := OfNat.ofNat 10, b := Bool.true : Foo } : Foo

tests/lean/eagerCoeExpansion.lean.expected.out

@@ -8,18 +8,18 @@ fun (a : Nat) =>
     (@Eq.{1} Bool
       (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      true)
+      Bool.true)
     (instDecidableEqBool
       (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      true)
+      Bool.true)
     (@Eq.{1} Bool
       (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
-      true)
+      Bool.true)
     (@Eq.{1} Bool
       (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
-      true)
+      Bool.true)
 def s : Option Nat :=
 HOrElse.hOrElse (ConstantFunction.f myFun 3) fun x => ConstantFunction.f myFun 4

tests/lean/interactive/hover.lean

@@ -101,3 +101,16 @@ example : Id Nat := do
   n := 2
 --^ textDocument/hover
   n
+
+
+constant foo : Nat
+
+#check _root_.foo
+       --^ textDocument/hover
+
+namespace Bar
+
+constant foo : Nat
+
+#check _root_.foo
+       --^ textDocument/hover

tests/lean/interactive/hover.lean.expected.out

@@ -91,3 +91,15 @@ null
 {"range":
  {"start": {"line": 100, "character": 2}, "end": {"line": 100, "character": 3}},
  "contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 107, "character": 9}}
+{"range":
+ {"start": {"line": 107, "character": 7},
+  "end": {"line": 107, "character": 17}},
+ "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 114, "character": 9}}
+{"range":
+ {"start": {"line": 114, "character": 7},
+  "end": {"line": 114, "character": 17}},
+ "contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}}

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

tests/lean/interactive/hoverDot.lean.expected.out

@@ -3,47 +3,52 @@
 {"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":
  {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}},
  "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"}}