Automatically enable inlay hints in Lean buffers.

leanprover/lean4#6768 is now merged (hooray!) and means that Lean shows
useful information like the use of auto-implicits via inlay hints.
This functionality is already available on Lean4 HEAD, and will shortly
be available in nightlies (and then in a release candidate).

Note that Neovim does not enable them by default, but this is mostly
because exactly what is shown in inlay hints varies widely by language
-- and here, it seems more reasonable that they be enabled by default in
Lean.

We do so only buffer-locally, and users can opt out of this by setting
`enabled = false` in the new `inlay_hint` config table.

(This also shouldn't interfere if any user is calling
`vim.lsp.inlay_hint.enable()` themselves already).

Author: Julian

ftplugin/lean/lean.lua

@@ -37,4 +37,8 @@ if config.mappings == true then
   require('lean').use_suggested_mappings(0)
 end
 
+if config.inlay_hint.enabled then
+  vim.lsp.inlay_hint.enable(true, { bufnr = 0 })
+end
+
 vim.bo.modifiable = config.ft:should_modify()

lua/lean/config.lua

@@ -11,6 +11,7 @@
 ---@field ft? lean.ft.Config filetype configuration
 ---@field abbreviations? lean.abbreviations.Config abbreviaton configuration
 ---@field infoview? lean.infoview.Config infoview configuration
+---@field inlay_hint? lean.inlay_hint.Config inlay hint configuration
 ---@field lsp? table language server configuration
 ---@field progress_bars? table progress bar configuration
 ---@field stderr? table stderr window configuration
@@ -21,6 +22,7 @@
 
 ---@class lean.MergedConfig: lean.Config
 ---@field ft lean.ft.MergedConfig filetype configuration
+---@field inlay_hint lean.inlay_hint.Config inlay hint configuration
 ---@field log Log log any messages from lean.nvim's internals
 
 ---@class lean.abbreviations.Config
@@ -38,6 +40,14 @@
 ---@field view_options? InfoviewViewOptions
 ---@field severity_markers? table<lsp.DiagnosticSeverity, string> characters to use for denoting diagnostic severity
 
+---Lean uses inlay hints to surface things like auto-implicits of a function.
+---
+---We enable them by default in Lean buffers, but they can be disabled if
+---desired below. Note that they are not enabled globally in Neovim by default
+---(as what exactly is shown in inlay hints can vary widely by language).
+---@class lean.inlay_hint.Config
+---@field enabled? boolean whether to automatically enable inlay hints
+
 ---@type lean.MergedConfig
 local DEFAULTS = {
   mappings = false,
@@ -89,6 +99,9 @@ local DEFAULTS = {
       'hint:\n',
     },
   },
+
+  ---@type lean.inlay_hint.Config
+  inlay_hint = { enabled = true },
 }
 
 ---Load our merged configuration merging user configuration with any defaults.