More minor typing improvements.

lua/lean/infoview/components.lua

@@ -41,7 +41,7 @@ local function goal_header(goals)
 end
 
 ---The current (tactic) goal state.
----@param goal table: a Lean `plainGoal` LSP response
+---@param goal PlainGoal: a Lean `plainGoal` LSP response
 ---@return Element[]
 function components.plain_goal(goal)
   if type(goal) ~= 'table' or not goal.goals then
@@ -515,7 +515,7 @@ end
 ---@param params lsp.TextDocumentPositionParams
 ---@param sess? Subsession
 ---@param use_widgets? boolean
----@return Element[] goal
+---@return Element[]? goal
 ---@return LspError? error
 function components.goal_at(params, sess, use_widgets)
   local goal, err
@@ -540,7 +540,7 @@ end
 ---@param params lsp.TextDocumentPositionParams
 ---@param sess? Subsession
 ---@param use_widgets? boolean
----@return Element[]
+---@return Element[]?
 ---@return LspError?
 function components.term_goal_at(params, sess, use_widgets)
   local term_goal, err
@@ -565,7 +565,7 @@ end
 ---@param params lsp.TextDocumentPositionParams
 ---@param sess? Subsession
 ---@param use_widgets? boolean
----@return Element[]
+---@return Element[]?
 ---@return LspError?
 function components.diagnostics_at(params, sess, use_widgets)
   local uri = params.textDocument.uri

lua/lean/lsp.lua

@@ -24,19 +24,23 @@ function lsp.enable(opts)
   require('lspconfig').leanls.setup(opts)
 end
 
----Find the vim.lsp.Client attached to the given buffer.
+---Find the `vim.lsp.Client` attached to the given buffer.
 ---@param bufnr number
 ---@return vim.lsp.Client
 function lsp.client_for(bufnr)
   local clients = vim.lsp.get_clients { name = 'leanls', bufnr = bufnr }
   return clients[1]
 end
 
+---@class PlainGoal
+---@field rendered string The goals as pretty-printed Markdown, or something like "no goals" if accomplished.
+---@field goals string[] The pretty-printed goals, empty if all accomplished.
+
 ---Fetch goal state information from the server (async).
 ---@param params lsp.TextDocumentPositionParams
 ---@param bufnr number
----@return any error
----@return any plain_goal
+---@return LspError? error
+---@return PlainGoal? plain_goal
 function lsp.plain_goal(params, bufnr)
   local client = lsp.client_for(bufnr)
   if not client then
@@ -50,11 +54,15 @@ function lsp.plain_goal(params, bufnr)
   return util.client_a_request(client, '$/lean/plainGoal', params)
 end
 
+---@class PlainTermGoal
+---@field goal string
+---@field range lsp.Range
+
 ---Fetch term goal state information from the server (async).
 ---@param params lsp.TextDocumentPositionParams
 ---@param bufnr number
----@return any error
----@return any plain_term_goal
+---@return LspError? error
+---@return PlainTermGoal? plain_term_goal
 function lsp.plain_term_goal(params, bufnr)
   local client = lsp.client_for(bufnr)
   if not client then
@@ -68,7 +76,7 @@ end
 ---@field processing LeanFileProgressProcessingInfo[]
 
 ---Called when `$/lean/fileProgress` is triggered.
----@param err table?
+---@param err LspError?
 ---@param params LeanFileProgressParams
 function lsp.handlers.file_progress_handler(err, params)
   if err ~= nil then

lua/lean/rpc.lua

@@ -97,7 +97,6 @@ function Session:release_now(refs)
   if #self.to_release == 0 or self:is_closed() then
     return
   end
-  ---@diagnostic disable-next-line: undefined-field
   self.client.notify('$/lean/rpc/release', {
     uri = self.uri,
     sessionId = self.session_id,