From b02b15f8cae2d3fc57134d309c9e790b9670bdc1 Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Tue, 6 Sep 2022 17:15:36 -0700 Subject: [PATCH 1/2] Fix idempotency issue It turns out that most of these come from the `_DEFAULTS` pattern. This is because of the following: original state: ```lua tbl = { _DEFAULTS = ... } ``` after configuration with empty table, `tbl = vim.tbl_extend(tbl._DEFAULTS, {})` which practically replaces `tbl` by `tbl._DEFAULTS`: ```lua tbl = { ... } ``` after this, the next call to `vim.tbl_extend(tbl._DEFAULTS, {})` fails, as `tbl._DEFAULTS` is nil. The solution to this is to just call `vim.tbl_extend(tbl, ...)` and store the defaults in `tbl` itself. The `._DEFAULTS` field can be preserved by copying to it after initialization. Also `command` has been replaced with `command!` in vimscript and `autocmd`s have been wrapped in an `augroup` which resets its state each call. This is also common practice that avoids duplicate autocommands. Fixes #145 --- lua/lean/commands.lua | 10 +++---- lua/lean/ft.lua | 2 +- lua/lean/infoview.lua | 58 +++++++++++++++++++------------------- lua/lean/init.lua | 46 +++++++++++++++--------------- lua/lean/progress_bars.lua | 17 +++++------ 5 files changed, 68 insertions(+), 65 deletions(-) diff --git a/lua/lean/commands.lua b/lua/lean/commands.lua index d1bc4767..71d1e9cb 100644 --- a/lua/lean/commands.lua +++ b/lua/lean/commands.lua @@ -116,11 +116,11 @@ end function commands.enable() vim.cmd[[ - 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! 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() ]] end diff --git a/lua/lean/ft.lua b/lua/lean/ft.lua index 99ecd7dc..c5d59225 100644 --- a/lua/lean/ft.lua +++ b/lua/lean/ft.lua @@ -21,7 +21,7 @@ function ft.enable(opts) -- this means we have to manage it global_default_managed = true end - options= vim.tbl_extend("force", options._DEFAULTS, opts) + options= vim.tbl_extend("force", options, opts) if global_default_managed then lean_nvim_default_filetype = options.default end diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua index 8203926a..da349c83 100644 --- a/lua/lean/infoview.lua +++ b/lua/lean/infoview.lua @@ -20,35 +20,35 @@ local infoview = { debug = false, } local options = { - _DEFAULTS = { - width = 50, - height = 20, - horizontal_position = 'bottom', - separate_tab = false, - - autoopen = true, - autopause = false, - indicators = "auto", - lean3 = { show_filter = true, mouse_events = false }, - show_processing = true, - show_no_info_message = false, - use_widgets = true, - - mappings = { - ['K'] = 'click', - [''] = 'click', - ['gd'] = 'go_to_def', - ['gD'] = 'go_to_decl', - ['gy'] = 'go_to_type', - ['I'] = 'mouse_enter', - ['i'] = 'mouse_leave', - [''] = 'clear_all', - ['C'] = 'clear_all', - [''] = 'goto_last_window', - } + width = 50, + height = 20, + horizontal_position = 'bottom', + separate_tab = false, + + autoopen = true, + autopause = false, + indicators = "auto", + lean3 = { show_filter = true, mouse_events = false }, + show_processing = true, + show_no_info_message = false, + use_widgets = true, + + mappings = { + ['K'] = 'click', + [''] = 'click', + ['gd'] = 'go_to_def', + ['gD'] = 'go_to_decl', + ['gy'] = 'go_to_type', + ['I'] = 'mouse_enter', + ['i'] = 'mouse_leave', + [''] = 'clear_all', + ['C'] = 'clear_all', + [''] = 'goto_last_window', } } +options._DEFAULTS = vim.deepcopy(options) + --- An individual pin. ---@class Pin ---@field id string @a label to identify the pin @@ -1039,13 +1039,13 @@ end --- Enable and open the infoview across all Lean buffers. function infoview.enable(opts) - options = vim.tbl_extend("force", options._DEFAULTS, opts) + options = vim.tbl_extend("force", options, opts) infoview.mappings = options.mappings infoview.enabled = true infoview.set_autoopen(options.autoopen) set_augroup("LeanInfoviewInit", [[ - autocmd FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('')) - autocmd FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('')) + autocmd! FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('')) + autocmd! FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('')) ]]) end diff --git a/lua/lean/init.lua b/lua/lean/init.lua index 4953c3e7..2082a194 100644 --- a/lua/lean/init.lua +++ b/lua/lean/init.lua @@ -43,7 +43,6 @@ function lean.setup(opts) opts.infoview = opts.infoview or {} require'lean.infoview'.enable(opts.infoview) - require'lean.commands'.enable() opts.lsp3 = opts.lsp3 or {} @@ -64,31 +63,34 @@ function lean.setup(opts) if opts.stderr.enable ~= false then require'lean.stderr'.enable(opts.stderr or {}) end vim.cmd[[ - command LeanRestartFile :lua require'lean.lsp'.restart_file() - command LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file() - - command LeanInfoviewToggle :lua require'lean.infoview'.toggle() - command LeanInfoviewPinTogglePause :lua require'lean.infoview'.pin_toggle_pause() - command LeanInfoviewAddPin :lua require'lean.infoview'.add_pin() - command LeanInfoviewClearPins :lua require'lean.infoview'.clear_pins() - command LeanInfoviewSetDiffPin :lua require'lean.infoview'.set_diff_pin() - command LeanInfoviewClearDiffPin :lua require'lean.infoview'.clear_diff_pin() - command LeanInfoviewToggleAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(true) - command LeanInfoviewToggleNoClearAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(false) - command LeanInfoviewEnableWidgets :lua require'lean.infoview'.enable_widgets() - command LeanInfoviewDisableWidgets :lua require'lean.infoview'.disable_widgets() - command LeanGotoInfoview :lua require'lean.infoview'.go_to() - - command LeanAbbreviationsReverseLookup :lua require'lean.abbreviations'.show_reverse_lookup() - - command LeanSorryFill :lua require'lean.sorry'.fill() - command LeanTryThis :lua require'lean.trythis'.swap() + command! LeanRestartFile :lua require'lean.lsp'.restart_file() + command! LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file() + + command! LeanInfoviewToggle :lua require'lean.infoview'.toggle() + command! LeanInfoviewPinTogglePause :lua require'lean.infoview'.pin_toggle_pause() + command! LeanInfoviewAddPin :lua require'lean.infoview'.add_pin() + command! LeanInfoviewClearPins :lua require'lean.infoview'.clear_pins() + command! LeanInfoviewSetDiffPin :lua require'lean.infoview'.set_diff_pin() + command! LeanInfoviewClearDiffPin :lua require'lean.infoview'.clear_diff_pin() + command! LeanInfoviewToggleAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(true) + command! LeanInfoviewToggleNoClearAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(false) + command! LeanInfoviewEnableWidgets :lua require'lean.infoview'.enable_widgets() + command! LeanInfoviewDisableWidgets :lua require'lean.infoview'.disable_widgets() + command! LeanGotoInfoview :lua require'lean.infoview'.go_to() + + command! LeanAbbreviationsReverseLookup :lua require'lean.abbreviations'.show_reverse_lookup() + + command! LeanSorryFill :lua require'lean.sorry'.fill() + command! LeanTryThis :lua require'lean.trythis'.swap() ]] if opts.mappings == true then vim.cmd[[ - autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true) - autocmd FileType lean lua require'lean'.use_suggested_mappings(true) + augroup lean_nvim_mappings + autocmd! + autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true) + autocmd FileType lean lua require'lean'.use_suggested_mappings(true) + augroup END ]] end diff --git a/lua/lean/progress_bars.lua b/lua/lean/progress_bars.lua index 8b84a84e..d06b1481 100644 --- a/lua/lean/progress_bars.lua +++ b/lua/lean/progress_bars.lua @@ -1,7 +1,8 @@ local progress = require('lean.progress') -local M = {} -local options = { _DEFAULTS = { priority = 10, character = '⋯' } } +local progress_bars = {} +local options = { priority = 10, character = '⋯' } +options._DEFAULTS = vim.deepcopy(options) local sign_group_name = 'leanSignProgress' local sign_name = 'leanSignProgress' @@ -41,8 +42,8 @@ end -- Table from bufnr to timer object. local timers = {} -function M.update(params) - if not M.enabled then return end +function progress_bars.update(params) + if not progress_bars.enabled then return end -- TODO FIXME can potentially create new buffer local bufnr = vim.uri_to_bufnr(params.textDocument.uri) @@ -54,15 +55,15 @@ function M.update(params) end end -function M.enable(opts) - options = vim.tbl_extend("force", options._DEFAULTS, opts) +function progress_bars.enable(opts) + options = vim.tbl_extend("force", options, opts) vim.fn.sign_define(sign_name, { text = options.character, texthl = 'leanSignProgress', }) vim.cmd[[hi def leanSignProgress guifg=orange ctermfg=215]] - M.enabled = true + progress_bars.enabled = true end -return M +return progress_bars From 6bfcc5175d890523d3ca61ababfdc0a069610710 Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Tue, 6 Sep 2022 17:45:40 -0700 Subject: [PATCH 2/2] Add test showing idempotency test plan: ``` $ TEST_FILE=lua/tests/setup_spec.lua ./lua/tests/scripts/run_tests.sh ======================================== Testing: lua/tests/setup_spec.lua Success || lean.setup Does not crash when loaded twice Success: 1 Failed : 0 Errors : 0 ======================================== ``` --- lua/tests/setup_spec.lua | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 lua/tests/setup_spec.lua diff --git a/lua/tests/setup_spec.lua b/lua/tests/setup_spec.lua new file mode 100644 index 00000000..a5d49477 --- /dev/null +++ b/lua/tests/setup_spec.lua @@ -0,0 +1,6 @@ +describe('lean.setup', function() + it('Does not crash when loaded twice', function() + require('lean').setup {} + require('lean').setup {} + end) +end)