From e217e5eff207c2136a8c3ff65454a04a9dbc4284 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Fri, 18 Oct 2024 16:37:04 -0400 Subject: [PATCH] Standardize some whitespace around comments/lua docstrings. Even though --- Foo --- @param bar --- @returns baz (with the space) looks nicer, vimcats cannot deal with it it seems, and requres `---@param` with no space. Sigh, wonderful, but ok. --- doc/lean.txt | 94 +++++++++++------- doc/tags | 2 + lua/lean/_util.lua | 29 +++--- lua/lean/abbreviations.lua | 18 ++-- lua/lean/config.lua | 2 +- lua/lean/health.lua | 4 +- lua/lean/infoview.lua | 132 ++++++++++++------------- lua/lean/infoview/components.lua | 38 +++---- lua/lean/init.lua | 8 +- lua/lean/lsp.lua | 14 +-- lua/lean/progress.lua | 14 +-- lua/lean/rpc.lua | 4 +- lua/lean/satellite.lua | 10 +- lua/lean/sorry.lua | 2 +- lua/lean/stderr.lua | 4 +- lua/lean/tui.lua | 8 +- lua/lean/widgets.lua | 44 ++++----- lua/telescope/_extensions/loogle.lua | 10 +- spec/helpers.lua | 44 ++++----- spec/infoview/autoopen_custom_spec.lua | 1 + spec/infoview/autoupdate_spec.lua | 10 +- spec/infoview/pin_spec.lua | 1 + spec/infoview/tooltips_spec.lua | 4 +- spec/infoview/widgets_spec.lua | 2 +- spec/lsp_spec.lua | 2 +- spec/tui_spec.lua | 2 +- syntax/leaninfo.lua | 2 +- 27 files changed, 266 insertions(+), 239 deletions(-) diff --git a/doc/lean.txt b/doc/lean.txt index d55e7d1a..141dee27 100644 --- a/doc/lean.txt +++ b/doc/lean.txt @@ -31,10 +31,10 @@ lean.use_suggested_mappings({bufnr?}) *lean.use_suggested_mappings* lean.current_search_paths() *lean.current_search_paths* - Return the current Lean search path. + Return the current Lean search path. - Includes both the Lean core libraries as well as project-specific - directories. + Includes both the Lean core libraries as well as project-specific + directories. ============================================================================== @@ -68,14 +68,14 @@ InfoviewViewOptions *InfoviewViewOptions* Pin *Pin* - An individual pin. + An individual pin. Fields: ~ {id} (string) @a label to identify the pin Info *Info* - An individual info. + An individual info. Fields: ~ {pin} (Pin) @@ -83,7 +83,7 @@ Info *Info* Infoview *Infoview* - A "view" on an info (i.e. window). + A "view" on an info (i.e. window). Fields: ~ {info} (Info) @@ -91,7 +91,7 @@ Infoview *Infoview* infoview.enable_debug() *infoview.enable_debug* - Enables printing of extra debugging information in the infoview. + Enables printing of extra debugging information in the infoview. InfoviewNewArgs *InfoviewNewArgs* @@ -110,98 +110,98 @@ FilterSelection *FilterSelection* infoview.close_all() *infoview.close_all* - Close all open infoviews (across all tabs). + Close all open infoviews (across all tabs). infoview.__update_pin_by_uri({uri}) *infoview.__update_pin_by_uri* - Update pins corresponding to the given URI. + Update pins corresponding to the given URI. Parameters: ~ {uri} (string) infoview.__update_pin_positions() *infoview.__update_pin_positions* - on_lines callback to update pins position according to the given textDocument/didChange parameters. + on_lines callback to update pins position according to the given textDocument/didChange parameters. infoview.enable() *infoview.enable* - Enable and open the infoview across all Lean buffers. + Enable and open the infoview across all Lean buffers. infoview.set_autoopen() *infoview.set_autoopen* - Set whether a new infoview is automatically opened when entering Lean buffers. + Set whether a new infoview is automatically opened when entering Lean buffers. infoview.set_autopause() *infoview.set_autopause* - Set whether a new pin is automatically paused. + Set whether a new pin is automatically paused. infoview.get_current_infoview() *infoview.get_current_infoview* - Get the infoview corresponding to the current window. + Get the infoview corresponding to the current window. Returns: ~ (Infoview) infoview.open() *infoview.open* - Open the current infoview (or ensure it is already open). + Open the current infoview (or ensure it is already open). infoview.close() *infoview.close* - Close the current infoview (or ensure it is already closed). + Close the current infoview (or ensure it is already closed). infoview.toggle() *infoview.toggle* - Toggle whether the current infoview is opened or closed. + Toggle whether the current infoview is opened or closed. infoview.pin_toggle_pause() *infoview.pin_toggle_pause* - Toggle whether the current pin receives updates. + Toggle whether the current pin receives updates. infoview.add_pin() *infoview.add_pin* - Add a pin to the current cursor location. + Add a pin to the current cursor location. infoview.set_diff_pin() *infoview.set_diff_pin* - Set the location for a diff pin to the current cursor location. + Set the location for a diff pin to the current cursor location. infoview.clear_pins() *infoview.clear_pins* - Clear any pins in the current infoview. + Clear any pins in the current infoview. infoview.clear_diff_pin() *infoview.clear_diff_pin* - Clear a diff pin in the current infoview. + Clear a diff pin in the current infoview. infoview.toggle_auto_diff_pin() *infoview.toggle_auto_diff_pin* - Toggle whether "auto-diff" mode is active for the current infoview. + Toggle whether "auto-diff" mode is active for the current infoview. infoview.enable_widgets() *infoview.enable_widgets* - Enable widgets in the current infoview. + Enable widgets in the current infoview. infoview.disable_widgets() *infoview.disable_widgets* - Disable widgets in the current infoview. + Disable widgets in the current infoview. infoview.go_to() *infoview.go_to* - Move the cursor to the infoview window. + Move the cursor to the infoview window. infoview.reposition() *infoview.reposition* - Move the current infoview to the appropriate spot based on the - current screen dimensions. - Does nothing if there are more than 2 open windows. + Move the current infoview to the appropriate spot based on the + current screen dimensions. + Does nothing if there are more than 2 open windows. infoview.select_view_options() *infoview.select_view_options* - Interactively set some view options for the infoview. + Interactively set some view options for the infoview. - Does not persist the selected options; if you wish to permanently affect - which hypotheses are shown, set them in your lean.nvim configuration. + Does not persist the selected options; if you wish to permanently affect + which hypotheses are shown, set them in your lean.nvim configuration. ============================================================================== @@ -210,14 +210,21 @@ infoview.select_view_options() *infoview.select_view_options* Support for abbreviations (unicode character replacement). abbreviations.load() *abbreviations.load* - Load the Lean abbreviations as a Lua table. + Load the Lean abbreviations as a Lua table. abbreviations.reverse_lookup() *abbreviations.reverse_lookup* + Retrieve the table of abbreviations that would produce the given symbol. + + Allows for trailing junk. E.g. `λean` will produce information about `λ`. + + The result is a table keyed by the length of the prefix match, and + whose value is sorted such that shorter abbreviation suggestions are + first. abbreviations.show_reverse_lookup() *abbreviations.show_reverse_lookup* - Show a preview window with the reverse-lookup of the current character. + Show a preview window with the reverse-lookup of the current character. abbreviations.convert() *abbreviations.convert* @@ -266,6 +273,10 @@ satellite.nvim integration *lean.satellite* See https://github.com/lewis6991/satellite.nvim/blob/main/HANDLERS.md + *Lean.SatelliteConfig* +Lean.SatelliteConfig : Satellite.Handlers.BaseConfig + + ============================================================================== LSP *lean.lsp* @@ -275,7 +286,7 @@ lsp.enable() *lsp.enable* lsp.client_for({bufnr}) *lsp.client_for* - Find the vim.lsp.Client attached to the given buffer. + Find the vim.lsp.Client attached to the given buffer. Parameters: ~ {bufnr} (number) @@ -285,6 +296,7 @@ lsp.client_for({bufnr}) *lsp.client_for* lsp.plain_goal({params}, {bufnr}) *lsp.plain_goal* + Fetch goal state information from the server (async). Parameters: ~ {params} (lsp.TextDocumentPositionParams) @@ -296,6 +308,7 @@ lsp.plain_goal({params}, {bufnr}) *lsp.plain_goal* lsp.plain_term_goal({params}, {bufnr}) *lsp.plain_term_goal* + Fetch term goal state information from the server (async). Parameters: ~ {params} (lsp.TextDocumentPositionParams) @@ -306,6 +319,13 @@ lsp.plain_term_goal({params}, {bufnr}) *lsp.plain_term_goal* (any) plain_term_goal +LeanFileProgressParams *LeanFileProgressParams* + + Fields: ~ + {textDocument} (lsp.VersionedTextDocumentIdentifier) + {processing} (LeanFileProgressProcessingInfo[]) + + *lsp.handlers.file_progress_handler* lsp.handlers.file_progress_handler({params}) @@ -337,7 +357,7 @@ stderr.show({message}) *stderr.show* stderr.enable() *stderr.enable* - Enable teeing stderr output somewhere (to a second visible buffer by default). + Enable teeing stderr output somewhere (to a second visible buffer by default). ============================================================================== @@ -350,7 +370,7 @@ Client-side sorrying *lean.sorry* behavior. sorry.fill() *sorry.fill* - Fill the current cursor position with `sorry`s to discharge all goals. + Fill the current cursor position with `sorry`s to discharge all goals. vim:tw=78:ts=8:noet:ft=help:norl: diff --git a/doc/tags b/doc/tags index 4a2edb61..9efb1a71 100644 --- a/doc/tags +++ b/doc/tags @@ -3,6 +3,8 @@ Info lean.txt /*Info* Infoview lean.txt /*Infoview* InfoviewNewArgs lean.txt /*InfoviewNewArgs* InfoviewViewOptions lean.txt /*InfoviewViewOptions* +Lean.SatelliteConfig lean.txt /*Lean.SatelliteConfig* +LeanFileProgressParams lean.txt /*LeanFileProgressParams* LoogleResult lean.txt /*LoogleResult* Pin lean.txt /*Pin* abbreviations.convert lean.txt /*abbreviations.convert* diff --git a/lua/lean/_util.lua b/lua/lean/_util.lua index 385ef5ea..4054b817 100644 --- a/lua/lean/_util.lua +++ b/lua/lean/_util.lua @@ -1,11 +1,14 @@ --- Stuff that should live in some standard library. +---@brief [[ +--- Stuff that should live in some standard library. +---@brief ]] + local Job = require 'plenary.job' local a = require 'plenary.async' -- local control = require'plenary.async.control' local M = {} ---- Return an array-like table with a value repeated the given number of times. +---Return an array-like table with a value repeated the given number of times. function M.tbl_repeat(value, times) local result = {} for _ = 1, times do @@ -14,7 +17,7 @@ function M.tbl_repeat(value, times) return result end ---- Fetch the diagnostics for all Lean LSP clients from the current buffer. +---Fetch the diagnostics for all Lean LSP clients from the current buffer. ---@param opts? table ---@param bufnr? number buffer handle or 0 for current, defaults to current ---@return vim.Diagnostic[] diagnostics the relevant Lean diagnostics @@ -56,11 +59,11 @@ function M.create_buf(params) return bufnr end ---- Run a subprocess, blocking on exit, and returning its stdout. +---Run a subprocess, blocking on exit, and returning its stdout. --- ---- Unlike `system()`, we don't mix stdout and stderr, and unlike ---- `vim.uv.spawn`, we wait for process exit and collect the output. ---- @return table: the lines of stdout of the exited process +---Unlike `system()`, we don't mix stdout and stderr, and unlike +---`vim.uv.spawn`, we wait for process exit and collect the output. +---@return table: the lines of stdout of the exited process function M.subprocess_check_output(opts, timeout) timeout = timeout or 10000 @@ -97,16 +100,16 @@ local function max_common_indent(str) return common_indent end ---- Dedent a multi-line string. +---Dedent a multi-line string. --- ---- REPLACEME: plenary.nvim has a version of this but it has odd behavior. +---REPLACEME: plenary.nvim has a version of this but it has odd behavior. function M.dedent(str) str = str:gsub('^ +', ''):gsub('\n *$', '\n') -- trim leading/trailing space local prefix = max_common_indent(str) return str:gsub('\n' .. prefix, '\n') end ---- Build a single-line string out a multiline one, replacing \n with spaces. +---Build a single-line string out a multiline one, replacing \n with spaces. function M.s(str) return M.dedent(str):gsub('\n', ' ') end @@ -122,7 +125,7 @@ function M.client_a_request(client, request, params) end, 1)() end --- simple alternative to vim.lsp.util._make_floating_popup_size +---Simple alternative to vim.lsp.util._make_floating_popup_size function M.make_floating_popup_size(contents) return unpack(vim.iter(contents):fold({ 0, 0 }, function(acc, line) local width, height = unpack(acc) @@ -137,7 +140,7 @@ end ---@field textDocument { uri: string } ---@field position { line: uinteger, character: uinteger } ---- Check that the given position parameters are valid given the buffer they correspond to. +---Check that the given position parameters are valid given the buffer they correspond to. ---@param params UIParams @parameters to verify ---@return boolean function M.position_params_valid(params) @@ -188,7 +191,7 @@ local function buf_get_line_ending(bufnr) end ---@private ---- Returns full text of buffer {bufnr} as a string. +---Returns full text of buffer {bufnr} as a string. --- ---@param bufnr (number) Buffer handle, or 0 for current. ---@return string # Buffer text as string. diff --git a/lua/lean/abbreviations.lua b/lua/lean/abbreviations.lua index ae738f4e..9feb25c4 100644 --- a/lua/lean/abbreviations.lua +++ b/lua/lean/abbreviations.lua @@ -8,7 +8,7 @@ local abbreviations = {} local _MEMOIZED = nil ---- Load the Lean abbreviations as a Lua table. +---Load the Lean abbreviations as a Lua table. function abbreviations.load() if _MEMOIZED ~= nil then return _MEMOIZED @@ -20,13 +20,13 @@ function abbreviations.load() return _MEMOIZED end ---- Retrieve the table of abbreviations that would produce the given symbol. --- --- Allows for trailing junk. E.g. `λean` will produce information about `λ`. --- --- The result is a table keyed by the length of the prefix match, and --- whose value is sorted such that shorter abbreviation suggestions are --- first. +---Retrieve the table of abbreviations that would produce the given symbol. +--- +---Allows for trailing junk. E.g. `λean` will produce information about `λ`. +--- +---The result is a table keyed by the length of the prefix match, and +---whose value is sorted such that shorter abbreviation suggestions are +---first. function abbreviations.reverse_lookup(symbol_plus_unknown) local reverse = {} for key, value in pairs(abbreviations.load()) do @@ -43,7 +43,7 @@ function abbreviations.reverse_lookup(symbol_plus_unknown) return reverse end ---- Show a preview window with the reverse-lookup of the current character. +---Show a preview window with the reverse-lookup of the current character. function abbreviations.show_reverse_lookup() local col = vim.api.nvim_win_get_cursor(0)[2] + 1 local char = vim.api.nvim_get_current_line():sub(col) diff --git a/lua/lean/config.lua b/lua/lean/config.lua index 096349c3..46f35876 100644 --- a/lua/lean/config.lua +++ b/lua/lean/config.lua @@ -77,7 +77,7 @@ local DEFAULTS = { }, } ---- Load our merged configuration merging user configuration with any defaults. +---Load our merged configuration merging user configuration with any defaults. ---@return lean.MergedConfig return function() ---@type lean.Config diff --git a/lua/lean/health.lua b/lua/lean/health.lua index a160ab1b..0c8d72b0 100644 --- a/lua/lean/health.lua +++ b/lua/lean/health.lua @@ -37,9 +37,9 @@ local function no_timers() end return { - --- Check whether lean.nvim is healthy. + ---Check whether lean.nvim is healthy. --- - --- Call me via `:checkhealth lean`. + ---Call me via `:checkhealth lean`. check = function() vim.health.start 'lean.nvim' neovim_is_new_enough() diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua index d704f4ba..a1fa61dd 100644 --- a/lua/lean/infoview.lua +++ b/lua/lean/infoview.lua @@ -18,7 +18,7 @@ local infoview = { ---@type table _by_tabpage = {}, - --- Whether to print additional debug information in the infoview. + ---Whether to print additional debug information in the infoview. ---@type boolean debug = false, } @@ -59,7 +59,7 @@ options._DEFAULTS = vim.deepcopy(options) ---@field show_let_values boolean show let-value bodies ---@field reverse boolean order hypotheses bottom-to-top ---- An individual pin. +---An individual pin. ---@class Pin ---@field id string @a label to identify the pin ---@field private __data_element Element @@ -75,7 +75,7 @@ options._DEFAULTS = vim.deepcopy(options) local Pin = { __extmark_ns = vim.api.nvim_create_namespace 'lean.pins' } Pin.__index = Pin ---- An individual info. +---An individual info. ---@class Info ---@field pin Pin ---@field pins Pin[] @@ -90,7 +90,7 @@ Pin.__index = Pin local Info = {} Info.__index = Info ---- A "view" on an info (i.e. window). +---A "view" on an info (i.e. window). ---@class Infoview ---@field info Info ---@field window integer @@ -103,7 +103,7 @@ Info.__index = Info local Infoview = {} Infoview.__index = Infoview ---- Enables printing of extra debugging information in the infoview. +---Enables printing of extra debugging information in the infoview. function infoview.enable_debug() infoview.debug = true end @@ -114,7 +114,7 @@ end ---@field horizontal_position? "top"|"bottom" ---@field separate_tab? boolean ---- Create a new infoview. +---Create a new infoview. ---@param obj InfoviewNewArgs ---@return Infoview function Infoview:new(obj) @@ -139,7 +139,7 @@ function Infoview:__should_be_vertical() end end ---- Open this infoview if it isn't already open +---Open this infoview if it isn't already open function Infoview:open() if self.window then return @@ -252,8 +252,8 @@ function Infoview:reposition() end end ---- Move the cursor to the given (1-indexed) goal. ---- @param n? integer the goal number to move to, defaulting to the first +---Move the cursor to the given (1-indexed) goal. +---@param n? integer the goal number to move to, defaulting to the first function Infoview:move_cursor_to_goal(n) n = n or 1 local lines = vim.api.nvim_buf_get_lines(self.info.__renderer.buf, 0, -1, false) @@ -270,7 +270,7 @@ function Infoview:move_cursor_to_goal(n) end end ---- Enter the given infoview (i.e. set the current window to it). +---Enter the given infoview (i.e. set the current window to it). function Infoview:enter() if self.window and vim.api.nvim_win_is_valid(self.window) then vim.api.nvim_set_current_win(self.window) @@ -281,7 +281,7 @@ end ---@field description string ---@field option string ---- Interactively set view options for this infoview. +---Interactively set view options for this infoview. function Infoview:select_view_options() ---@type FilterSelection[] local choices = { @@ -341,9 +341,9 @@ function Infoview:select_view_options() end) end ---- API for opening an auxilliary window relative to the current infoview window. ---- @param buf number @buffer to put in the new window ---- @return number? @new window handle or nil if the infoview is closed +---API for opening an auxilliary window relative to the current infoview window. +---@param buf number @buffer to put in the new window +---@return number? @new window handle or nil if the infoview is closed function Infoview:__open_win(buf) if not self.window then return @@ -403,9 +403,9 @@ function Infoview:__refresh() self.info.__win_event_disable = false end ---- Filter the pins from this infoview which are relevant to a given buffer. ---- @param uri string @the URI which filters the pins ---- @return Pin[] +---Filter the pins from this infoview which are relevant to a given buffer. +---@param uri string @the URI which filters the pins +---@return Pin[] function Infoview:pins_for(uri) if not self.window then return {} @@ -432,7 +432,7 @@ function Infoview:__update() pcall(info.move_pin, info, util.make_position_params()) end ---- Either open or close a diff window for this infoview depending on whether its info has a diff pin. +---Either open or close a diff window for this infoview depending on whether its info has a diff pin. function Infoview:__refresh_diff() if not self.window then return @@ -461,7 +461,7 @@ function Infoview:__refresh_diff() self:__refresh() end ---- Close this infoview's diff window. +---Close this infoview's diff window. function Infoview:__close_diff() if not self.window or not self.__diff_win then return @@ -485,7 +485,7 @@ function Infoview:__close_diff() self:__refresh() end ---- Close this infoview. +---Close this infoview. function Infoview:close() if not self.window then return @@ -500,7 +500,7 @@ function Infoview:__was_closed() self.info.__renderer:event 'clear_all' -- Ensure tooltips close. end ---- Retrieve the contents of the infoview as a table. +---Retrieve the contents of the infoview as a table. ---@param start_line? number ---@param end_line? number function Infoview:get_lines(start_line, end_line) @@ -513,13 +513,13 @@ function Infoview:get_lines(start_line, end_line) return vim.api.nvim_buf_get_lines(self.info.__renderer.buf, start_line, end_line, true) end ---- Retrieve a specific line from the infoview window. +---Retrieve a specific line from the infoview window. ---@param line number function Infoview:get_line(line) return self:get_lines(line, line + 1)[1] end ---- Retrieve the contents of the diff window as a table. +---Retrieve the contents of the diff window as a table. ---@param start_line? number ---@param end_line? number function Infoview:get_diff_lines(start_line, end_line) @@ -532,7 +532,7 @@ function Infoview:get_diff_lines(start_line, end_line) return vim.api.nvim_buf_get_lines(self.info.__diff_renderer.buf, start_line, end_line, true) end ---- Toggle this infoview being open. +---Toggle this infoview being open. function Infoview:toggle() if self.window then self:close() @@ -541,7 +541,7 @@ function Infoview:toggle() end end ---- Update the info contents. +---Update the info contents. local function update_current_infoview() if vim.bo.filetype ~= 'lean' then return @@ -553,7 +553,7 @@ local function update_current_infoview() return current_infoview:__update() end ---- Set the currently active Lean buffer to update the infoview. +---Set the currently active Lean buffer to update the infoview. function Infoview:focus_on_current_buffer() if self.window then vim.api.nvim_create_autocmd({ 'CursorMoved', 'CursorMovedI' }, { @@ -700,7 +700,7 @@ function Info:__clear_diff_pin() self:render() end ---- Show a pin extmark if it is appropriate based on configuration. +---Show a pin extmark if it is appropriate based on configuration. function Info:__maybe_show_pin_extmark(...) if not options.indicators or options.indicators == 'never' then return @@ -712,7 +712,7 @@ function Info:__maybe_show_pin_extmark(...) self.pin:__show_extmark(...) end ---- Set the current window as the last window used to update this Info. +---Set the current window as the last window used to update this Info. function Info:set_last_window() self.last_window = vim.api.nvim_get_current_win() end @@ -788,7 +788,7 @@ function Info:__render_pins() end end ---- Update this info's physical contents. +---Update this info's physical contents. function Info:render() self:__render_pins() @@ -806,8 +806,8 @@ function Info:render() collectgarbage() -- FIXME: Why?? end ---- Update the diff pin to use the current pin's positon params if they are valid, ---- and the provided params if they are not. +---Update the diff pin to use the current pin's positon params if they are valid, +---and the provided params if they are not. ---@param params? UIParams function Info:__update_auto_diff_pin(params) if @@ -821,7 +821,7 @@ function Info:__update_auto_diff_pin(params) end end ---- Move the current pin to the specified location. +---Move the current pin to the specified location. ---@param params UIParams function Info:move_pin(params) if self.__auto_diff_pin then @@ -830,8 +830,8 @@ function Info:move_pin(params) self.pin:move(params) end ---- Toggle auto diff pin mode. ---- @param clear boolean @clear the pin when disabling auto diff pin mode? +---Toggle auto diff pin mode. +---@param clear boolean @clear the pin when disabling auto diff pin mode? function Info:__toggle_auto_diff_pin(clear) if self.__auto_diff_pin then self.__auto_diff_pin = false @@ -872,13 +872,13 @@ function Pin:new(obj) ) end ---- Enable widgets for this pin. +---Enable widgets for this pin. function Pin:enable_widgets() self.__use_widgets = true self:update() end ---- Disable widgets (in favor of plaintext goals) for this pin. +---Disable widgets (in favor of plaintext goals) for this pin. function Pin:disable_widgets() self.__use_widgets = false self:update() @@ -891,7 +891,7 @@ function Pin:__teardown() end end ---- Update pin extmark based on position, used when resetting pin position. +---Update pin extmark based on position, used when resetting pin position. ---@param params UIParams function Pin:__update_extmark(params) if not params then @@ -946,7 +946,7 @@ function Pin:__update_extmark_style(buf, line, col) self.__extmark_buf = buf end ---- Update pin position based on extmark, used directly when changing text, indirectly when setting position. +---Update pin position based on extmark, used directly when changing text, indirectly when setting position. function Pin:update_position() local extmark = self.__extmark if not extmark then @@ -1020,7 +1020,7 @@ function Pin:toggle_pause() end end ---- Triggered when manually moving a pin. +---Triggered when manually moving a pin. ---@param params UIParams function Pin:move(params) self:__update_extmark(params) @@ -1066,7 +1066,7 @@ end Pin.update = a.void(Pin.async_update) ---- async function to update this pin's contents given the current position. +---async function to update this pin's contents given the current position. function Pin:__update() local params = self.__position_params @@ -1123,14 +1123,14 @@ function Pin:__update() self.__data_element = new_data_element end ---- Close all open infoviews (across all tabs). +---Close all open infoviews (across all tabs). function infoview.close_all() for _, each in pairs(infoview._by_tabpage) do each:close() end end ---- Update pins corresponding to the given URI. +---Update pins corresponding to the given URI. ---@param uri string function infoview.__update_pin_by_uri(uri) for _, each in pairs(infoview._by_tabpage) do @@ -1140,7 +1140,7 @@ function infoview.__update_pin_by_uri(uri) end end ---- on_lines callback to update pins position according to the given textDocument/didChange parameters. +---on_lines callback to update pins position according to the given textDocument/didChange parameters. function infoview.__update_pin_positions(_, bufnr, _, _, _, _, _, _, _) local uri = vim.uri_from_bufnr(bufnr) for _, each in pairs(infoview._by_tabpage) do @@ -1167,7 +1167,7 @@ end -- __update_pin_positions local attached_buffers = {} ---- Callback when entering a Lean buffer. +---Callback when entering a Lean buffer. local function infoview_bufenter() -- Open an infoview for the current buffer if it isn't already open. local tabpage = vim.api.nvim_get_current_tabpage() @@ -1185,7 +1185,7 @@ local function infoview_bufenter() update_current_infoview() end ---- Enable and open the infoview across all Lean buffers. +---Enable and open the infoview across all Lean buffers. function infoview.enable(opts) options = vim.tbl_extend('force', options, opts) infoview.mappings = options.mappings @@ -1232,7 +1232,7 @@ function infoview.enable(opts) }) end ---- Set whether a new infoview is automatically opened when entering Lean buffers. +---Set whether a new infoview is automatically opened when entering Lean buffers. function infoview.set_autoopen(autoopen) if autoopen == true then autoopen = function() @@ -1246,18 +1246,18 @@ function infoview.set_autoopen(autoopen) options.autoopen = autoopen end ---- Set whether a new pin is automatically paused. +---Set whether a new pin is automatically paused. function infoview.set_autopause(autopause) options.autopause = autopause end ---- Get the infoview corresponding to the current window. +---Get the infoview corresponding to the current window. ---@return Infoview function infoview.get_current_infoview() return infoview._by_tabpage[vim.api.nvim_get_current_tabpage()] end ---- Open the current infoview (or ensure it is already open). +---Open the current infoview (or ensure it is already open). function infoview.open() local tabpage = vim.api.nvim_get_current_tabpage() local current_infoview = infoview.get_current_infoview() @@ -1269,7 +1269,7 @@ function infoview.open() return current_infoview end ---- Close the current infoview (or ensure it is already closed). +---Close the current infoview (or ensure it is already closed). function infoview.close() local current_infoview = infoview.get_current_infoview() if current_infoview then @@ -1277,7 +1277,7 @@ function infoview.close() end end ---- Toggle whether the current infoview is opened or closed. +---Toggle whether the current infoview is opened or closed. function infoview.toggle() local iv = infoview.get_current_infoview() if iv ~= nil then @@ -1287,7 +1287,7 @@ function infoview.toggle() end end ---- Toggle whether the current pin receives updates. +---Toggle whether the current pin receives updates. function infoview.pin_toggle_pause() local iv = infoview.get_current_infoview() if iv then @@ -1295,7 +1295,7 @@ function infoview.pin_toggle_pause() end end ---- Add a pin to the current cursor location. +---Add a pin to the current cursor location. function infoview.add_pin() if vim.bo.filetype ~= 'lean' then return @@ -1305,7 +1305,7 @@ function infoview.add_pin() current_infoview.info:add_pin() end ---- Set the location for a diff pin to the current cursor location. +---Set the location for a diff pin to the current cursor location. function infoview.set_diff_pin() if vim.bo.filetype ~= 'lean' then return @@ -1315,7 +1315,7 @@ function infoview.set_diff_pin() current_infoview.info:__set_diff_pin(util.make_position_params()) end ---- Clear any pins in the current infoview. +---Clear any pins in the current infoview. function infoview.clear_pins() local iv = infoview.get_current_infoview() if iv then @@ -1323,7 +1323,7 @@ function infoview.clear_pins() end end ---- Clear a diff pin in the current infoview. +---Clear a diff pin in the current infoview. function infoview.clear_diff_pin() local iv = infoview.get_current_infoview() if iv then @@ -1331,7 +1331,7 @@ function infoview.clear_diff_pin() end end ---- Toggle whether "auto-diff" mode is active for the current infoview. +---Toggle whether "auto-diff" mode is active for the current infoview. function infoview.toggle_auto_diff_pin(clear) if vim.bo.filetype ~= 'lean' then return @@ -1340,7 +1340,7 @@ function infoview.toggle_auto_diff_pin(clear) current_infoview.info:__toggle_auto_diff_pin(clear) end ---- Enable widgets in the current infoview. +---Enable widgets in the current infoview. function infoview.enable_widgets() local iv = infoview.get_current_infoview() if iv ~= nil then @@ -1348,7 +1348,7 @@ function infoview.enable_widgets() end end ---- Disable widgets in the current infoview. +---Disable widgets in the current infoview. function infoview.disable_widgets() local iv = infoview.get_current_infoview() if iv ~= nil then @@ -1356,7 +1356,7 @@ function infoview.disable_widgets() end end ---- Move the cursor to the infoview window. +---Move the cursor to the infoview window. function infoview.go_to() local curr_info = infoview.open().info -- if there is no last win, just go straight to the window itself @@ -1367,9 +1367,9 @@ function infoview.go_to() end end ---- Move the current infoview to the appropriate spot based on the ---- current screen dimensions. ---- Does nothing if there are more than 2 open windows. +---Move the current infoview to the appropriate spot based on the +---current screen dimensions. +---Does nothing if there are more than 2 open windows. function infoview.reposition() local iv = infoview.get_current_infoview() if iv then @@ -1377,10 +1377,10 @@ function infoview.reposition() end end ---- Interactively set some view options for the infoview. +---Interactively set some view options for the infoview. --- ---- Does not persist the selected options; if you wish to permanently affect ---- which hypotheses are shown, set them in your lean.nvim configuration. +---Does not persist the selected options; if you wish to permanently affect +---which hypotheses are shown, set them in your lean.nvim configuration. function infoview.select_view_options() infoview.open():select_view_options() end diff --git a/lua/lean/infoview/components.lua b/lua/lean/infoview/components.lua index e6816e92..43350d14 100644 --- a/lua/lean/infoview/components.lua +++ b/lua/lean/infoview/components.lua @@ -16,15 +16,15 @@ local components = { PROCESSING = Element:new { text = 'Processing file...', name = 'processing' }, } ---- Format a heading. +---Format a heading. local function H(contents) return ('▶ %s'):format(contents) end ---- Convert an LSP range to a human-readable, (1,1)-indexed string. +---Convert an LSP range to a human-readable, (1,1)-indexed string. --- ---- The (1, 1) indexing is to match the interface used interactively for ---- `gg` and `|`. +---The (1, 1) indexing is to match the interface used interactively for +---`gg` and `|`. local function range_to_string(range) return ('%d:%d-%d:%d'):format( range['start'].line + 1, @@ -40,7 +40,7 @@ local function goal_header(goals) or H(('%d goals\n'):format(#goals)) end ---- The current (tactic) goal state. +---The current (tactic) goal state. ---@param goal table: a Lean `plainGoal` LSP response ---@return Element[] function components.plain_goal(goal) @@ -77,7 +77,7 @@ function components.plain_goal(goal) } end ---- The current (term) goal state. +---The current (term) goal state. ---@param term_goal table: a Lean `plainTermGoal` LSP response ---@return Element[] function components.term_goal(term_goal) @@ -217,17 +217,17 @@ local function code_with_infos(t, sess) return element end ---- A hypothesis name which is accessible according to Lean's naming conventions. +---A hypothesis name which is accessible according to Lean's naming conventions. ---@param name string local function is_accessible(name) return name:sub(-#'✝') ~= '✝' end ---- Filter the hypotheses according to view options, then convert them to elements. ---- @param hyps InteractiveHypothesisBundle[] ---- @param opts InfoviewViewOptions ---- @param sess Subsession ---- @return Element? +---Filter the hypotheses according to view options, then convert them to elements. +---@param hyps InteractiveHypothesisBundle[] +---@param opts InfoviewViewOptions +---@param sess Subsession +---@return Element? local function to_hypotheses_element(hyps, opts, sess) ---@param hyp InteractiveHypothesisBundle local children = vim.iter(hyps):map(function(hyp) @@ -323,7 +323,7 @@ function components.interactive_goals(goal, sess) return { Element:new { name = 'interactive-goals', children = children } } end ---- The current (term) goal state. +---The current (term) goal state. ---@param goal InteractiveTermGoal ---@param sess Subsession ---@return Element[] @@ -345,14 +345,14 @@ function components.interactive_term_goal(goal, sess) } end ---- Diagnostic information for the current line from the Lean server. ---- @param uri string ---- @param line number ---- @return Element[] +---Diagnostic information for the current line from the Lean server. +---@param uri string +---@param line number +---@return Element[] function components.diagnostics(uri, line) local markers = config().infoview.severity_markers - --- @param diagnostic vim.Diagnostic + ---@param diagnostic vim.Diagnostic return vim.tbl_map(function(diagnostic) return Element:new { name = 'diagnostic', @@ -482,7 +482,7 @@ local function tagged_text_msg_embed(t, sess, parent_cls) return element end ---- Diagnostic information for the current line from the Lean server. +---Diagnostic information for the current line from the Lean server. ---@param line number ---@param diags InteractiveDiagnostic[] ---@param sess Subsession diff --git a/lua/lean/init.lua b/lua/lean/init.lua index 2407a659..27712b12 100644 --- a/lua/lean/init.lua +++ b/lua/lean/init.lua @@ -86,7 +86,7 @@ local lean = { vim.filetype.add { extension = { lean = 'lean' } } ---- Setup function to be run in your init.lua (or init.vim). +---Setup function to be run in your init.lua (or init.vim). ---@param opts lean.Config: Configuration options function lean.setup(opts) opts = opts or {} @@ -165,10 +165,10 @@ function lean.use_suggested_mappings(bufnr) end end ---- Return the current Lean search path. +---Return the current Lean search path. --- ---- Includes both the Lean core libraries as well as project-specific ---- directories. +---Includes both the Lean core libraries as well as project-specific +---directories. function lean.current_search_paths() local paths diff --git a/lua/lean/lsp.lua b/lua/lean/lsp.lua index 67525f60..598bedb8 100644 --- a/lua/lean/lsp.lua +++ b/lua/lean/lsp.lua @@ -24,7 +24,7 @@ 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) @@ -32,7 +32,7 @@ function lsp.client_for(bufnr) return clients[1] end --- Fetch goal state information from the server (async). +---Fetch goal state information from the server (async). ---@param params lsp.TextDocumentPositionParams ---@param bufnr number ---@return any error @@ -50,7 +50,7 @@ function lsp.plain_goal(params, bufnr) return util.client_a_request(client, '$/lean/plainGoal', params) end --- Fetch term goal state information from the server (async). +---Fetch term goal state information from the server (async). ---@param params lsp.TextDocumentPositionParams ---@param bufnr number ---@return any error @@ -63,11 +63,11 @@ function lsp.plain_term_goal(params, bufnr) return util.client_a_request(client, '$/lean/plainTermGoal', params) end ---- @class LeanFileProgressParams ---- @field textDocument lsp.VersionedTextDocumentIdentifier ---- @field processing LeanFileProgressProcessingInfo[] +---@class LeanFileProgressParams +---@field textDocument lsp.VersionedTextDocumentIdentifier +---@field processing LeanFileProgressProcessingInfo[] ---- Called when `$/lean/fileProgress` is triggered. +---Called when `$/lean/fileProgress` is triggered. ---@param err table? ---@param params LeanFileProgressParams function lsp.handlers.file_progress_handler(err, params) diff --git a/lua/lean/progress.lua b/lua/lean/progress.lua index b34a15d4..fee47476 100644 --- a/lua/lean/progress.lua +++ b/lua/lean/progress.lua @@ -7,7 +7,7 @@ local M = { AUTOCMD = 'LeanProgressUpdate', - --- @enum LeanFileProgressKind + ---@enum LeanFileProgressKind Kind = { processing = 1, fatal_error = 2, @@ -23,16 +23,16 @@ M.proc_infos = {} vim.cmd.hi 'def leanProgressBar guifg=orange ctermfg=215' ---- @param params LeanFileProgressParams +---@param params LeanFileProgressParams function M.update(params) M.proc_infos[params.textDocument.uri] = params.processing vim.api.nvim_exec_autocmds('User', { pattern = M.AUTOCMD }) end ---- Check if we're processing the given location, returning the kind if so. ---- Returns `nil` if we're not processing at the given location. ---- @param params lsp.TextDocumentPositionParams ---- @return LeanFileProgressKind? kind +---Check if we're processing the given location, returning the kind if so. +---Returns `nil` if we're not processing at the given location. +---@param params lsp.TextDocumentPositionParams +---@return LeanFileProgressKind? kind function M.at(params) local infos = M.proc_infos[params.textDocument.uri] if not infos then -- it's so early we don't even have any info yet @@ -41,7 +41,7 @@ function M.at(params) -- ignoring character for now (seems to always be 0) local line = params.position.line - --- @type LeanFileProgressProcessingInfo? + ---@type LeanFileProgressProcessingInfo? local info = vim.iter(infos):find(function(each) return (line >= each.range.start.line) and (line <= each.range['end'].line) end) diff --git a/lua/lean/rpc.lua b/lua/lean/rpc.lua index 533e09cb..22255358 100644 --- a/lua/lean/rpc.lua +++ b/lua/lean/rpc.lua @@ -161,7 +161,7 @@ function Session:call(pos, method, params) return result, err end ---- Map from bufnr to Session object. +---Map from bufnr to Session object. ---@type table local sessions = {} @@ -212,7 +212,7 @@ function Subsession:call(method, params) return self.sess:call(self.pos, method, params) end ---- Open an RPC session. +---Open an RPC session. ---@param params lsp.TextDocumentPositionParams ---@return Subsession function rpc.open(params) diff --git a/lua/lean/satellite.lua b/lua/lean/satellite.lua index 8f83a5d3..ea014e58 100644 --- a/lua/lean/satellite.lua +++ b/lua/lean/satellite.lua @@ -19,12 +19,12 @@ local progress = require 'lean.progress' local SYMBOL = '│' local HIGHLIGHT = 'leanProgressBar' ---- @type Satellite.Handler +---@type Satellite.Handler local handler = { name = 'lean.nvim', } ---- @class Lean.SatelliteConfig: Satellite.Handlers.BaseConfig +---@class Lean.SatelliteConfig: Satellite.Handlers.BaseConfig local config = { enable = true, overlap = true, @@ -38,8 +38,8 @@ local function setup_hl() }) end ---- @param user_config Satellite.Handlers.CursorConfig ---- @param update fun() +---@param user_config Satellite.Handlers.CursorConfig +---@param update fun() function handler.setup(user_config, update) config = vim.tbl_deep_extend('force', config, user_config) handler.config = config @@ -61,7 +61,7 @@ function handler.setup(user_config, update) end function handler.update(bufnr, winid) - local marks = {} --- @type Satellite.Mark[] + local marks = {} ---@type Satellite.Mark[] local infos = progress.proc_infos[vim.uri_from_bufnr(bufnr)] or {} local pred = async.winbuf_pred(bufnr, winid) diff --git a/lua/lean/sorry.lua b/lua/lean/sorry.lua index 01e8cf69..9ed11f59 100644 --- a/lua/lean/sorry.lua +++ b/lua/lean/sorry.lua @@ -29,7 +29,7 @@ local function calculate_indent(line) return string.rep(' ', indent) end ---- Fill the current cursor position with `sorry`s to discharge all goals. +---Fill the current cursor position with `sorry`s to discharge all goals. function sorry.fill() local params = vim.lsp.util.make_position_params() local responses = vim.lsp.buf_request_sync(0, '$/lean/plainGoal', params) diff --git a/lua/lean/stderr.lua b/lua/lean/stderr.lua index 012a816a..2df40777 100644 --- a/lua/lean/stderr.lua +++ b/lua/lean/stderr.lua @@ -13,7 +13,7 @@ local stderr = {} local current = {} local stderr_height ---- Open a window for the stderr buffer of the configured height. +---Open a window for the stderr buffer of the configured height. local function open_window(stderr_bufnr) local old_win = vim.api.nvim_get_current_win() @@ -57,7 +57,7 @@ function stderr.show(message) end) end ---- Enable teeing stderr output somewhere (to a second visible buffer by default). +---Enable teeing stderr output somewhere (to a second visible buffer by default). function stderr.enable(config) local on_lines = config.on_lines or stderr.show local old_error = log.error diff --git a/lua/lean/tui.lua b/lua/lean/tui.lua index b09ab78c..34ba8a3f 100644 --- a/lua/lean/tui.lua +++ b/lua/lean/tui.lua @@ -73,7 +73,7 @@ function Element.noop(text) } end ---- The empty element (with no content). +---The empty element (with no content). Element.EMPTY = Element:new {} ---@param children? Element[] @@ -231,7 +231,7 @@ local function take(arr, n) return res end --- Finds the innermost element satisfying a predicate +---Find the innermost element satisfying a predicate. ---@param path PathNode[] ---@param check fun(element:Element):any ---@return Element found The element satisfying check @@ -271,7 +271,7 @@ local function pos_to_raw_pos(pos, lines) return raw_pos end --- returns (0, 0)-indexed cursor position from raw byte position and list of lines +---Return (0, 0)-indexed cursor position from raw byte position and list of lines local function raw_pos_to_pos(raw_pos, lines) local line_num = 0 local rem_chars = raw_pos @@ -545,7 +545,7 @@ function BufRenderer:update_cursor(win) end end ---- Checks if two paths are equal, ignoring auxillary metadata (e.g. offsets) +---Checks if two paths are equal, ignoring auxillary metadata (e.g. offsets) ---@param path_a PathNode[]? @first path ---@param path_b PathNode[]? @second path local function path_equal(path_a, path_b) diff --git a/lua/lean/widgets.lua b/lua/lean/widgets.lua index 5b3b5871..cd7c4b8c 100644 --- a/lua/lean/widgets.lua +++ b/lua/lean/widgets.lua @@ -15,26 +15,26 @@ local dedent = require('lean._util').dedent ---@alias WidgetRenderer fun(self: Widget, props: any): Element[]? ---- A Lean user widget. ---- @class Widget ---- @field element WidgetRenderer +---A Lean user widget. +---@class Widget +---@field element WidgetRenderer local Widget = {} Widget.__index = Widget ---- @class WidgetNewArgs ---- @field element WidgetRenderer +---@class WidgetNewArgs +---@field element WidgetRenderer ---- Create a new Widget. ---- @param args WidgetNewArgs ---- @return Widget +---Create a new Widget. +---@param args WidgetNewArgs +---@return Widget function Widget:new(args) local obj = { element = args.element } return setmetatable(obj, self) end ---- A null widget which indicates it is standing in for one not-yet-supported. ---- @param id string the ID of the user widget we are not implementing ---- @return Widget +---A null widget which indicates it is standing in for one not-yet-supported. +---@param id string the ID of the user widget we are not implementing +---@return Widget function Widget.unsupported(id) return Widget:new { element = function() @@ -47,8 +47,8 @@ function Widget.unsupported(id) } end ---- A registry of `Widget`s which we essentially reimplement in Lua rather than ---- by executing their Javascript source modules. +---A registry of `Widget`s which we essentially reimplement in Lua rather than +---by executing their Javascript source modules. local BYPASSED_WIDGETS = vim.defaulttable(Widget.unsupported) ---Implement the Lean user widget with the given ID (by @@ -78,15 +78,15 @@ local function render(instance) return Widget.from_user_widget(instance):element(instance.props) end ---- @alias SuggestionText string +---@alias SuggestionText string ---- @class Suggestion ---- @field suggestion SuggestionText Text to be used as a replacement via a code action. ---- @field preInfo? string Optional info to be printed immediately before replacement text in a widget. ---- @field postInfo? string Optional info to be printed immediately after replacement text in a widget. +---@class Suggestion +---@field suggestion SuggestionText Text to be used as a replacement via a code action. +---@field preInfo? string Optional info to be printed immediately before replacement text in a widget. +---@field postInfo? string Optional info to be printed immediately after replacement text in a widget. ---- @class TryThisParams ---- @field suggestions Suggestion[] +---@class TryThisParams +---@field suggestions Suggestion[] ---@param props TryThisParams implement('Lean.Meta.Tactic.TryThis.tryThisWidget', function(_, props) @@ -102,8 +102,8 @@ implement('Lean.Meta.Tactic.TryThis.tryThisWidget', function(_, props) } end) ---- @class GoToModuleLinkParams ---- @field modName string the module to jump to +---@class GoToModuleLinkParams +---@field modName string the module to jump to ---A "jump to a module" which comes from `import-graph`. ---@param props GoToModuleLinkParams diff --git a/lua/telescope/_extensions/loogle.lua b/lua/telescope/_extensions/loogle.lua index 944a5065..c771dd84 100644 --- a/lua/telescope/_extensions/loogle.lua +++ b/lua/telescope/_extensions/loogle.lua @@ -12,8 +12,8 @@ local loogle = require 'lean.loogle' ---@field display string what to display in telescope for this result ---@field ordinal string how to sort this result in telescope ---- Use telescope to provide a Loogle API based type search ---- @param opts table Options for the telescope framework +---Use telescope to provide a Loogle API based type search +---@param opts table Options for the telescope framework local function telescope_loogle(opts) opts = vim.tbl_extend('keep', opts or {}, { debounce = 200 }) @@ -22,7 +22,7 @@ local function telescope_loogle(opts) prompt_title = 'Loogle', debounce = opts.debounce, finder = finders.new_dynamic { - --- @param prompt string the currently entered telescope prompt + ---@param prompt string the currently entered telescope prompt fn = function(prompt) if not prompt or prompt == '' then return nil @@ -39,8 +39,8 @@ local function telescope_loogle(opts) end return results end, - --- @param entry LoogleResult - --- @return LoogleTelescopeEntry + ---@param entry LoogleResult + ---@return LoogleTelescopeEntry entry_maker = function(entry) return { value = entry, diff --git a/spec/helpers.lua b/spec/helpers.lua index 796060e6..03ca3527 100644 --- a/spec/helpers.lua +++ b/spec/helpers.lua @@ -8,14 +8,14 @@ local util = require 'lean._util' local helpers = { _clean_buffer_counter = 1 } ---- Feed some keystrokes into the current buffer, replacing termcodes. +---Feed some keystrokes into the current buffer, replacing termcodes. function helpers.feed(text, feed_opts) feed_opts = feed_opts or 'mtx' local to_feed = vim.api.nvim_replace_termcodes(text, true, false, true) vim.api.nvim_feedkeys(to_feed, feed_opts, true) end ---- Insert some text into the current buffer. +---Insert some text into the current buffer. function helpers.insert(text, feed_opts) feed_opts = feed_opts or 'x' helpers.feed('i' .. text, feed_opts) @@ -34,12 +34,12 @@ function helpers.all_lean_extmarks(buffer, start, end_) return extmarks end ---- Move the cursor to a new location. +---Move the cursor to a new location. --- ---- Ideally this function wouldn't exist, and one would call ---- `vim.api.nvim_win_set_cursor` directly, but it does not fire `CursorMoved` ---- autocmds. This function exists therefore to make tests which have slightly ---- less implementation details in them (the manual firing of that autocmd). +---Ideally this function wouldn't exist, and one would call +---`vim.api.nvim_win_set_cursor` directly, but it does not fire `CursorMoved` +---autocmds. This function exists therefore to make tests which have slightly +---less implementation details in them (the manual firing of that autocmd). --- ---@param opts MoveCursorOpts function helpers.move_cursor(opts) @@ -62,7 +62,7 @@ end ---@field window? integer @the window handle. Defaults to the current window. ---@field to table @the new cursor position (1-row indexed, as per nvim_win_set_cursor) ---- Wait for all of the pins associated with the given infoview to finish loading/processing. +---Wait for all of the pins associated with the given infoview to finish loading/processing. ---@param iv? Infoview function helpers.wait_for_loading_pins(iv) iv = iv or infoview.get_current_infoview() @@ -121,11 +121,11 @@ local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) vim.api.nvim_buf_set_name(bufnr, unique_name) end ---- Create a clean Lean buffer with the given contents. --- --- Waits for the LSP to be ready before proceeding with a given callback. +---Create a clean Lean buffer with the given contents. +--- +---Waits for the LSP to be ready before proceeding with a given callback. -- --- Yes c(lean) may be a double entendre, and no I don't feel bad. +---Yes c(lean) may be a double entendre, and no I don't feel bad. function helpers.clean_buffer(contents, callback) local lines @@ -158,7 +158,7 @@ function helpers.clean_buffer(contents, callback) end end ---- Wait a few seconds for line diagnostics, erroring if none arrive. +---Wait a few seconds for line diagnostics, erroring if none arrive. function helpers.wait_for_line_diagnostics() local succeeded, _ = vim.wait(15000, function() if progress.at(vim.lsp.util.make_position_params()) == progress.Kind.processing then @@ -179,21 +179,21 @@ function helpers.wait_for_filetype() assert.message('filetype was never set').is_truthy(result) end ---- Assert about the current word. +---Assert about the current word. local function has_current_word(_, arguments) assert.is.equal(arguments[1], vim.fn.expand '') return true end assert:register('assertion', 'current_word', has_current_word) ---- Assert about the current line. +---Assert about the current line. local function has_current_line(_, arguments) assert.is.equal(arguments[1], vim.api.nvim_get_current_line()) return true end assert:register('assertion', 'current_line', has_current_line) ---- Assert about the current cursor location. +---Assert about the current cursor location. local function has_current_cursor(_, arguments) local window = arguments[1].window or 0 local got = vim.api.nvim_win_get_cursor(window) @@ -206,14 +206,14 @@ local function has_current_cursor(_, arguments) end assert:register('assertion', 'current_cursor', has_current_cursor) ---- Assert about the current tabpage. +---Assert about the current tabpage. local function has_current_tabpage(_, arguments) assert.is.equal(arguments[1], vim.api.nvim_get_current_tabpage()) return true end assert:register('assertion', 'current_tabpage', has_current_tabpage) ---- Assert about the current window. +---Assert about the current window. local function has_current_window(_, arguments) assert.is.equal(arguments[1], vim.api.nvim_get_current_win()) return true @@ -230,7 +230,7 @@ local function _expected(arguments) return expected end ---- Assert about the entire buffer contents. +---Assert about the entire buffer contents. local function has_buf_contents(_, arguments) local bufnr = arguments[1].bufnr or 0 local got = table.concat(vim.api.nvim_buf_get_lines(bufnr, 0, -1, false), '\n') @@ -239,7 +239,7 @@ local function has_buf_contents(_, arguments) end assert:register('assertion', 'contents', has_buf_contents) ---- Assert about the current infoview contents. +---Assert about the current infoview contents. local function has_infoview_contents(_, arguments) local expected = _expected(arguments) local target_infoview = arguments[1].infoview or infoview.get_current_infoview() @@ -272,7 +272,7 @@ local function has_infoview_contents(_, arguments) return true end ---- Assert about the current infoview contents without waiting for the pins to load. +---Assert about the current infoview contents without waiting for the pins to load. local function has_infoview_contents_nowait(_, arguments) local target_infoview = arguments[1].infoview or infoview.get_current_infoview() local got = table.concat(target_infoview:get_lines(), '\n') @@ -306,7 +306,7 @@ end assert:register('assertion', 'has_all', has_all) ---- Assert a tabpage has the given windows open in it. +---Assert a tabpage has the given windows open in it. local function has_open_windows(_, arguments) local expected if arguments.n == 1 and type(arguments[1]) == 'table' then diff --git a/spec/infoview/autoopen_custom_spec.lua b/spec/infoview/autoopen_custom_spec.lua index 705ff80c..7de75106 100644 --- a/spec/infoview/autoopen_custom_spec.lua +++ b/spec/infoview/autoopen_custom_spec.lua @@ -2,6 +2,7 @@ --- Tests for infoview autoopen as a function (where its return value decides --- whether to open the new infoview or not). ---@brief ]] + require 'spec.helpers' local fixtures = require 'spec.fixtures' local infoview = require 'lean.infoview' diff --git a/spec/infoview/autoupdate_spec.lua b/spec/infoview/autoupdate_spec.lua index 149e9ab8..2448193d 100644 --- a/spec/infoview/autoupdate_spec.lua +++ b/spec/infoview/autoupdate_spec.lua @@ -24,7 +24,7 @@ local fixtures = require 'spec.fixtures' local helpers = require 'spec.helpers' local infoview = require 'lean.infoview' ---- We turn widgets off here, but that shouldn't really be affecting updating. +-- We turn widgets off here, but that shouldn't really be affecting updating. require('lean').setup { infoview = { use_widgets = false } } describe('infoview content (auto-)update', function() @@ -256,10 +256,10 @@ describe('infoview content (auto-)update', function() end) it('autoupdates when contents are modified without the cursor moving', function() - --- FIXME: This test is meant to ensure that we re-send requests on ContentModified LSP - --- errors, but it doesn't seem to do that (it doesn't seem to do particularly that - --- even before being refactored though, as it passes with or without the relevant - --- lines in infoview.lua) + -- FIXME: This test is meant to ensure that we re-send requests on ContentModified LSP + -- errors, but it doesn't seem to do that (it doesn't seem to do particularly that + -- even before being refactored though, as it passes with or without the relevant + -- lines in infoview.lua) vim.cmd.edit { fixtures.project.child 'Test.lean', bang = true } helpers.move_cursor { to = { 23, 1 } } assert.infoview_contents.are [[ diff --git a/spec/infoview/pin_spec.lua b/spec/infoview/pin_spec.lua index 5cfb6542..d13fe694 100644 --- a/spec/infoview/pin_spec.lua +++ b/spec/infoview/pin_spec.lua @@ -1,6 +1,7 @@ ---@brief [[ --- Tests for the placing of infoview pins. ---@brief ]] + local helpers = require 'spec.helpers' local infoview = require 'lean.infoview' diff --git a/spec/infoview/tooltips_spec.lua b/spec/infoview/tooltips_spec.lua index dca4085f..b02a0c60 100644 --- a/spec/infoview/tooltips_spec.lua +++ b/spec/infoview/tooltips_spec.lua @@ -1,7 +1,7 @@ ---@brief [[ ----Tests for tooltips (rendered inside infoviews). +--- Tests for tooltips (rendered inside infoviews). --- ----Really this should combine with the user widget tests (which it preceeds). +--- Really this should combine with the user widget tests (which it preceeds). ---@brief ]] local helpers = require 'spec.helpers' diff --git a/spec/infoview/widgets_spec.lua b/spec/infoview/widgets_spec.lua index f9775c3d..b32a1fc1 100644 --- a/spec/infoview/widgets_spec.lua +++ b/spec/infoview/widgets_spec.lua @@ -1,5 +1,5 @@ ---@brief [[ ----Tests for Lean's (user) widgets. +--- Tests for Lean's (user) widgets. ---@brief ]] local Element = require('lean.tui').Element diff --git a/spec/lsp_spec.lua b/spec/lsp_spec.lua index 9a411f19..6c416307 100644 --- a/spec/lsp_spec.lua +++ b/spec/lsp_spec.lua @@ -1,5 +1,5 @@ ---@brief [[ ----Tests for basic (auto-)attaching of LSP clients. +--- Tests for basic (auto-)attaching of LSP clients. ---@brief ]] local fixtures = require 'spec.fixtures' diff --git a/spec/tui_spec.lua b/spec/tui_spec.lua index 5fa2a347..275d392d 100644 --- a/spec/tui_spec.lua +++ b/spec/tui_spec.lua @@ -1,5 +1,5 @@ ---@brief [[ ----Tests for the console UI framework in isolation from Lean-specific widgets. +--- Tests for the console UI framework in isolation from Lean-specific widgets. ---@brief ]] local helpers = require 'spec.helpers' diff --git a/syntax/leaninfo.lua b/syntax/leaninfo.lua index c464e073..ec0f2fb1 100644 --- a/syntax/leaninfo.lua +++ b/syntax/leaninfo.lua @@ -36,7 +36,7 @@ local HLGROUPS = { 'DiagnosticOk', } ---- @type string, string +---@type string, string local match, hlgroup for i, to_group in vim.iter(ipairs(HLGROUPS)) do match = config.severity_markers[i]:gsub('\n', [[\_$]])