feat: show declaration keywords in hovers

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -94,7 +94,7 @@ def handleHover (p : HoverParams)
         if let some range := ictx.info.range? then
           -- prefer info tree if at least as specific as parser docstring
           if stxDoc?.all fun (_, stxRange) => stxRange.includes range then
-            if let some hoverFmt ← ictx.info.fmtHover? ictx.ctx then
+            if let some hoverFmt ← ictx.info.fmtHover? ictx.ctx stack? then
               return mkHover (toString hoverFmt.fmt) range
 
       if let some (doc, range) := stxDoc? then

src/Lean/Server/InfoUtils.lean

@@ -310,7 +310,9 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
 
 
 /-- Construct a hover popup, if any, from an info node in a context.-/
-def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
+def Info.fmtHover?
+    (ci : ContextInfo) (i : Info) (stk? : Option Syntax.Stack) :
+    IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do
     let mut fmts := #[]
     let mut infos := ∅
@@ -346,7 +348,8 @@ where
       let tpFmt ← Meta.ppExpr tp
       if let .const c _ := e then
         let eFmt ← PrettyPrinter.ppSignature c
-        return (some { eFmt with fmt := f!"```lean\n{eFmt.fmt}\n```" }, ← fmtModule? c)
+        let kw ← constDeclKw c
+        return (some { eFmt with fmt := f!"```lean\n{kw ++ eFmt.fmt}\n```" }, ← fmtModule? c)
       let eFmt ← Meta.ppExpr e
       -- Try not to show too scary internals
       let showTerm := if let .fvar _ := e then
@@ -362,6 +365,98 @@ where
       return (some f!"```lean\n{fi.fieldName} : {tpFmt}\n```", none)
     | _ => return (none, none)
 
+  /--
+  Attempts to discover which keyword was used to declare a constant so it can be shown in the hover.
+  -/
+  constDeclKw (c : Name) : MetaM Format := do
+    match (← getEnv).find? c with
+    | some (.axiomInfo ..) => pure "axiom "
+    | some (.defnInfo {type, ..}) =>
+      -- Don't show "def" for syntax categories
+      if (← Meta.isDefEq type (.const ``Lean.Parser.Category [])) then
+        pure .nil
+      -- nor for "syntax" declarations
+      else if (← Meta.isDefEq type (.const ``Lean.ParserDescr [])) then
+        pure .nil
+      else if (← Meta.isInstance c) then
+        pure "instance "
+      else if let .reducible := (← getReducibilityStatus c) then
+        pure "abbrev "
+      else
+        if let some stk := stk? then
+          if let some d := (← declSyntaxKw c stk) then
+            return d
+        pure "def "
+    | some (.inductInfo ..) =>
+      let x := ci.parentDecl?
+      if isClass (← getEnv) c then
+        if isStructure (← getEnv) c then
+          return "class "
+        else
+          return "class inductive"
+      else if isStructure (← getEnv) c then
+        return "structure "
+      else
+        -- When hovering on the header of a class or structure type, the environment used for the
+        -- query does not yet contain structure info. Examining the syntax for which the hover is
+        -- being produced can reveal whether the site in question is part of such a hover.
+        if let some stk := stk? then
+          if let some d := (← declSyntaxKw c stk) then
+            return d
+        return s!"inductive "
+    | some (.opaqueInfo ..) => pure "opaque "
+    | some (.thmInfo ..) => pure "theorem "
+    | some (.quotInfo ..)
+    | some (.ctorInfo ..)
+    | some (.recInfo ..)
+    | none => pure .nil
+
+  -- Loops outwards from the hovered syntax until it finds a declaration with a name that matches
+  -- the hovered constant. If it finds it, the declaration is examined to determine the appropriate
+  -- keyword.
+  declSyntaxKw (c : Name) (stk : Syntax.Stack) : MetaM (Option String) := do
+    for (stx, n) in stk do
+      if stx.getKind == ``Lean.Parser.Command.declaration then
+        let mods := stx[0]
+        if stx[1].getKind == ``Lean.Parser.Command.structure then
+          let isClass := stx[1][0].getKind == ``Parser.Command.classTk
+          let declId := stx[1][1]
+          let declName := getDeclName (← getVisibility ⟨mods⟩) declId
+          if declName == c then
+            if isClass then return some "class " else return some "structure "
+        else if stx[1].getKind == ``Lean.Parser.Command.classInductive then
+          let declId := stx[1][1]
+          let declName := getDeclName (← getVisibility ⟨mods⟩) declId
+          if declName == c then
+            return some "class inductive "
+        else if stx[1].getKind == ``Lean.Parser.Command.instance then
+          if let some declId := stx[1][3].getOptional? then
+            let declName := getDeclName (← getVisibility ⟨mods⟩) declId
+            if declName == c then
+              return some "instance "
+        else if stx[1].getKind == ``Lean.Parser.Command.abbrev then
+          let declId := stx[1][1]
+          let declName := getDeclName (← getVisibility ⟨mods⟩) declId
+          if declName == c then
+            return some "abbrev "
+
+    return none
+
+  getDeclName (visibility : Visibility) (declId : Syntax) : Name :=
+    let declName := ci.currNamespace ++ (expandDeclIdCore declId).1
+    if let .private := visibility then
+      mkPrivateName ci.env declName
+    else declName
+
+  getVisibility (mods : TSyntax ``Lean.Parser.Command.declModifiers) : MetaM Visibility :=
+      match mods.raw[2].getOptional? with
+      | none   => pure .regular
+      | some v =>
+        let kind := v.getKind
+        if kind == ``Parser.Command.private then pure .private
+        else if kind == ``Parser.Command.protected then pure .protected
+        else pure .regular
+
   isAtomicFormat : Format → Bool
     | Std.Format.text _    => true
     | Std.Format.group f _ => isAtomicFormat f

tests/lean/interactive/amb.lean.expected.out

@@ -3,10 +3,10 @@
 {"range":
  {"start": {"line": 17, "character": 19}, "end": {"line": 17, "character": 20}},
  "contents":
- {"value": "```lean\nFoo.f (n : Nat) : Bool\n```", "kind": "markdown"}}
+ {"value": "```lean\ndef Foo.f (n : Nat) : Bool\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file:///amb.lean"},
  "position": {"line": 19, "character": 19}}
 {"range":
  {"start": {"line": 19, "character": 19}, "end": {"line": 19, "character": 20}},
  "contents":
- {"value": "```lean\nBoo.f (n : String) : String\n```", "kind": "markdown"}}
+ {"value": "```lean\ndef Boo.f (n : String) : String\n```", "kind": "markdown"}}

tests/lean/interactive/explicitAppInstHole.lean.expected.out

@@ -4,5 +4,5 @@
  {"start": {"line": 4, "character": 29}, "end": {"line": 4, "character": 30}},
  "contents":
  {"value":
-  "```lean\ninstDecidableTrue : Decidable True\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n\n***\n*import Init.Core*",
+  "```lean\ninstance instDecidableTrue : Decidable True\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n\n***\n*import Init.Core*",
   "kind": "markdown"}}