Fix idempotency issue

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
 

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

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',
-      ['<CR>'] = 'click',
-      ['gd'] = 'go_to_def',
-      ['gD'] = 'go_to_decl',
-      ['gy'] = 'go_to_type',
-      ['I'] = 'mouse_enter',
-      ['i'] = 'mouse_leave',
-      ['<Esc>'] = 'clear_all',
-      ['C'] = 'clear_all',
-      ['<LocalLeader><Tab>'] = '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',
+    ['<CR>'] = 'click',
+    ['gd'] = 'go_to_def',
+    ['gD'] = 'go_to_decl',
+    ['gy'] = 'go_to_type',
+    ['I'] = 'mouse_enter',
+    ['i'] = 'mouse_leave',
+    ['<Esc>'] = 'clear_all',
+    ['C'] = 'clear_all',
+    ['<LocalLeader><Tab>'] = '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('<afile>'))
-    autocmd FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
+    autocmd! FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
+    autocmd! FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
   ]])
 end
 

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
 

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

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)