diff --git a/lua/lean/commands.lua b/lua/lean/commands.lua index b8550cc2..78522d17 100644 --- a/lua/lean/commands.lua +++ b/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,7 +64,9 @@ 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() @@ -68,7 +74,7 @@ function commands.show_line_diagnostics() 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)() diff --git a/lua/lean/init.lua b/lua/lean/init.lua index 1227a8b4..b6c354e0 100644 --- a/lua/lean/init.lua +++ b/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()