Enable diagnostics in the LeanLineDiagnostics command.

(And corresponding Lua API).

They were previously disabled simply because we used to not support
interactive diagnostics.

This also adds a `LeanPlainDiagnostics` command, paralleling the other
`LeanPlain*` commands, should someone not want widgets enabled.

lua/lean/commands.lua

@@ -42,6 +42,8 @@ local function show_popup_or_error(elements, err)
   end
 end
 
+---Show the goal for the current cursor position in a popup.
+---@param use_widgets boolean? enable widgets in the popup?
 function commands.show_goal(use_widgets)
   local params = vim.lsp.util.make_position_params()
 
@@ -51,6 +53,8 @@ function commands.show_goal(use_widgets)
   end)()
 end
 
+---Show the term goal for the current cursor position in a popup.
+---@param use_widgets boolean? enable widgets in the popup?
 function commands.show_term_goal(use_widgets)
   local params = vim.lsp.util.make_position_params()
 
@@ -60,15 +64,17 @@ function commands.show_term_goal(use_widgets)
   end)()
 end
 
-function commands.show_line_diagnostics()
+---Show diagnostics for the current cursor position in a popup.
+---@param use_widgets boolean? enable widgets in the popup?
+function commands.show_line_diagnostics(use_widgets)
   local params = vim.lsp.util.make_position_params()
 
   a.void(function()
     local diagnostics, err
     if progress.at(params) == progress.Kind.processing then
       err = 'Processing...'
     else
-      diagnostics, err = components.diagnostics_at(params, nil, false)
+      diagnostics, err = components.diagnostics_at(params, nil, use_widgets)
     end
     show_popup_or_error(diagnostics, err)
   end)()

lua/lean/init.lua

@@ -129,12 +129,14 @@ function lean.setup(opts)
     command! LeanRestartFile :lua require'lean.lsp'.restart_file()
     command! LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file()
 
-    command! LeanPlainGoal :lua require'lean.commands'.show_goal(false)
-    command! LeanPlainTermGoal :lua require'lean.commands'.show_term_goal(false)
     command! LeanGoal :lua require'lean.commands'.show_goal()
     command! LeanTermGoal :lua require'lean.commands'.show_term_goal()
     command! LeanLineDiagnostics :lua require'lean.commands'.show_line_diagnostics()
 
+    command! LeanPlainGoal :lua require'lean.commands'.show_goal(false)
+    command! LeanPlainTermGoal :lua require'lean.commands'.show_term_goal(false)
+    command! LeanPlainDiagnostics :lua require'lean.commands'.show_line_diagnostics(false)
+
     command! LeanGotoInfoview :lua require'lean.infoview'.go_to()
     command! LeanInfoviewToggle :lua require'lean.infoview'.toggle()